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

Theorem rabid2 3107
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 2729 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
2 pm4.71 661 . . . 4 ((𝑥𝐴𝜑) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝜑)))
32albii 1744 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
41, 3bitr4i 267 . 2 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴𝜑))
5 df-rab 2916 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
65eqeq2i 2633 . 2 (𝐴 = {𝑥𝐴𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)})
7 df-ral 2912 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
84, 6, 73bitr4i 292 1 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wcel 1987  {cab 2607  wral 2907  {crab 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-rab 2916
This theorem is referenced by:  rabxm  3935  iinrab2  4549  riinrab  4562  class2seteq  4793  dmmptg  5591  wfisg  5674  dmmptd  5981  fneqeql  6281  fmpt  6337  zfrep6  7081  axdc2lem  9214  ioomax  12190  iccmax  12191  hashbc  13175  lcmf0  15271  dfphi2  15403  phiprmpw  15405  phisum  15419  isnsg4  17558  symggen2  17812  psgnfvalfi  17854  lssuni  18859  psr1baslem  19474  psgnghm2  19846  ocv0  19940  dsmmfi  20001  frlmfibas  20024  frlmlbs  20055  ordtrest2lem  20917  comppfsc  21245  xkouni  21312  xkoccn  21332  tsmsfbas  21841  clsocv  22957  ehlbase  23102  ovolicc2lem4  23195  itg2monolem1  23423  musum  24817  lgsquadlem2  25006  umgr2v2evd2  26309  frgrregorufr0  27047  ubthlem1  27572  xrsclat  29462  psgndmfi  29628  ordtrest2NEWlem  29747  hasheuni  29925  measvuni  30055  imambfm  30102  subfacp1lem6  30872  connpconn  30922  cvmliftmolem2  30969  cvmlift2lem12  31001  tfisg  31414  frinsg  31440  poimirlem28  33066  fdc  33170  isbnd3  33212  pmap1N  34530  pol1N  34673  dia1N  35819  dihwN  36055  vdioph  36820  fiphp3d  36860  dmmptdf  38888  stirlinglem14  39608  suppdm  41585
  Copyright terms: Public domain W3C validator