MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabid2 Structured version   Visualization version   GIF version

Theorem rabid2 3255
Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
rabid2 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabid2
StepHypRef Expression
1 abeq2 2868 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
2 pm4.71 665 . . . 4 ((𝑥𝐴𝜑) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝜑)))
32albii 1894 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
41, 3bitr4i 267 . 2 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴𝜑))
5 df-rab 3057 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
65eqeq2i 2770 . 2 (𝐴 = {𝑥𝐴𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)})
7 df-ral 3053 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
84, 6, 73bitr4i 292 1 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1628   = wceq 1630  wcel 2137  {cab 2744  wral 3048  {crab 3052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-ral 3053  df-rab 3057
This theorem is referenced by:  rabxm  4102  iinrab2  4733  riinrab  4746  class2seteq  4980  dmmptg  5791  wfisg  5874  dmmptd  6183  fneqeql  6486  fmpt  6542  zfrep6  7297  axdc2lem  9460  ioomax  12439  iccmax  12440  hashbc  13427  lcmf0  15547  dfphi2  15679  phiprmpw  15681  phisum  15695  isnsg4  17836  symggen2  18089  psgnfvalfi  18131  lssuni  19140  psr1baslem  19755  psgnghm2  20127  ocv0  20221  dsmmfi  20282  frlmfibas  20305  frlmlbs  20336  ordtrest2lem  21207  comppfsc  21535  xkouni  21602  xkoccn  21622  tsmsfbas  22130  clsocv  23247  ehlbase  23392  ovolicc2lem4  23486  itg2monolem1  23714  musum  25114  lgsquadlem2  25303  umgr2v2evd2  26631  frgrregorufr0  27476  ubthlem1  28033  xrsclat  29987  psgndmfi  30153  ordtrest2NEWlem  30275  hasheuni  30454  measvuni  30584  imambfm  30631  subfacp1lem6  31472  connpconn  31522  cvmliftmolem2  31569  cvmlift2lem12  31601  tfisg  32019  frpoinsg  32045  frinsg  32049  poimirlem28  33748  fdc  33852  isbnd3  33894  pmap1N  35554  pol1N  35697  dia1N  36842  dihwN  37078  vdioph  37843  fiphp3d  37883  dmmptdf  39914  stirlinglem14  40805  fvmptrabdm  41815  suppdm  42808
  Copyright terms: Public domain W3C validator