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

Theorem rabid2 2717
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 2388 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
2 pm4.71 611 . . . 4  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  <->  ( x  e.  A  /\  ph )
) )
32albii 1553 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
41, 3bitr4i 243 . 2  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  ->  ph ) )
5 df-rab 2552 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2293 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2548 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
84, 6, 73bitr4i 268 1  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1684   {cab 2269   A.wral 2543   {crab 2547
This theorem is referenced by:  rabxm  3477  iinrab2  3965  riinrab  3977  class2seteq  4179  dmmptg  5170  fneqeql  5633  fmpt  5681  zfrep6  5748  axdc2lem  8074  ioomax  10724  iccmax  10725  hashbc  11391  dfphi2  12842  phiprmpw  12844  isnsg4  14660  lssuni  15697  psr1baslem  16264  ocv0  16577  ordtrest2lem  16933  xkouni  17294  xkoccn  17313  tsmsfbas  17810  clsocv  18677  ovolicc2lem4  18879  itg2monolem1  19105  musum  20431  lgsquadlem2  20594  ubthlem1  21449  hasheuni  23453  measvuni  23542  imambfm  23567  subfacp1lem6  23716  conpcon  23766  cvmliftmolem2  23813  cvmlift2lem12  23845  vdgr1d  23894  vdgr1b  23895  tfisg  24204  wfisg  24209  frinsg  24245  comppfsc  26307  fdc  26455  isbnd3  26508  vdioph  26859  fiphp3d  26902  dsmmfi  27204  frlmlbs  27249  symggen2  27412  psgnghm2  27438  matbas2  27475  phisum  27518  stirlinglem14  27836  pmap1N  29956  pol1N  30099  dia1N  31243  dihwN  31479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-rab 2552
  Copyright terms: Public domain W3C validator