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

Theorem rabid2 3382
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 2945 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
2 pm4.71 558 . . . 4 ((𝑥𝐴𝜑) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝜑)))
32albii 1811 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
41, 3bitr4i 279 . 2 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴𝜑))
5 df-rab 3147 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
65eqeq2i 2834 . 2 (𝐴 = {𝑥𝐴𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)})
7 df-ral 3143 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
84, 6, 73bitr4i 304 1 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wcel 2105  {cab 2799  wral 3138  {crab 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-rab 3147
This theorem is referenced by:  rabxm  4339  iinrab2  4984  riinrab  4998  class2seteq  5247  dmmptg  6090  wfisg  6177  dmmptd  6487  fneqeql  6809  fmpt  6867  zfrep6  7647  axdc2lem  9859  ioomax  12801  iccmax  12802  hashbc  13801  lcmf0  15968  dfphi2  16101  phiprmpw  16103  phisum  16117  isnsg4  18259  symggen2  18530  psgnfvalfi  18572  lssuni  19642  psr1baslem  20283  psgnghm2  20655  ocv0  20751  dsmmfi  20812  frlmfibas  20836  frlmlbs  20871  ordtrest2lem  21741  comppfsc  22070  xkouni  22137  xkoccn  22157  tsmsfbas  22665  clsocv  23782  ehlbase  23947  ovolicc2lem4  24050  itg2monolem1  24280  musum  25696  lgsquadlem2  25885  umgr2v2evd2  27237  frgrregorufr0  28031  ubthlem1  28575  xrsclat  30595  psgndmfi  30668  ordtrest2NEWlem  31065  hasheuni  31244  measvuni  31373  imambfm  31420  subfacp1lem6  32330  connpconn  32380  cvmliftmolem2  32427  cvmlift2lem12  32459  tfisg  32953  frpoinsg  32979  frinsg  32985  poimirlem28  34802  fdc  34903  isbnd3  34945  pmap1N  36785  pol1N  36928  dia1N  38071  dihwN  38307  vdioph  39256  fiphp3d  39296  dmmptdf  41368  stirlinglem14  42253  fvmptrabdm  43373  suppdm  44463
  Copyright terms: Public domain W3C validator