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

Theorem rabid2 3004
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  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rabid2
StepHypRef Expression
1 abeq2 2544 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
2 pm4.71 634 . . . 4  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  <->  ( x  e.  A  /\  ph )
) )
32albii 1687 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
41, 3bitr4i 255 . 2  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  ->  ph ) )
5 df-rab 2782 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2438 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2778 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
84, 6, 73bitr4i 280 1  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1867   {cab 2405   A.wral 2773   {crab 2777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-ral 2778  df-rab 2782
This theorem is referenced by:  rabxm  3782  iinrab2  4356  riinrab  4369  class2seteq  4584  dmmptg  5343  wfisg  5425  dmmptd  5717  fneqeql  5996  fmpt  6049  zfrep6  6766  axdc2lem  8867  ioomax  11698  iccmax  11699  hashbc  12600  lcmf0  14567  dfphi2  14680  phiprmpw  14682  isnsg4  16804  symggen2  17056  psgnfvalfi  17098  lssuni  18091  psr1baslem  18706  psgnghm2  19073  ocv0  19164  dsmmfi  19225  frlmfibas  19248  frlmlbs  19279  ordtrest2lem  20143  comppfsc  20471  xkouni  20538  xkoccn  20558  tsmsfbas  21066  clsocv  22107  ehlbase  22251  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  itg2monolem1  22582  musum  23980  lgsquadlem2  24143  vdgr1d  25473  vdgr1b  25474  frgraregorufr0  25622  ubthlem1  26354  xrsclat  28276  psgndmfi  28445  ordtrest2NEWlem  28564  hasheuni  28742  measvuni  28872  imambfm  28920  subfacp1lem6  29693  conpcon  29743  cvmliftmolem2  29790  cvmlift2lem12  29822  tfisg  30241  frinsg  30267  poimirlem28  31672  fdc  31778  isbnd3  31820  pmap1N  33041  pol1N  33184  dia1N  34330  dihwN  34566  vdioph  35331  fiphp3d  35371  phisum  35779  stirlinglem14  37522  suppdm  39077
  Copyright terms: Public domain W3C validator