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

Theorem rabid2 2730
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 2401 . . 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 1556 . . 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 2565 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2306 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2561 . 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 1530    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556   {crab 2560
This theorem is referenced by:  rabxm  3490  iinrab2  3981  riinrab  3993  class2seteq  4195  dmmptg  5186  fneqeql  5649  fmpt  5697  zfrep6  5764  axdc2lem  8090  ioomax  10740  iccmax  10741  hashbc  11407  dfphi2  12858  phiprmpw  12860  isnsg4  14676  lssuni  15713  psr1baslem  16280  ocv0  16593  ordtrest2lem  16949  xkouni  17310  xkoccn  17329  tsmsfbas  17826  clsocv  18693  ovolicc2lem4  18895  itg2monolem1  19121  musum  20447  lgsquadlem2  20610  ubthlem1  21465  hasheuni  23468  measvuni  23557  imambfm  23582  subfacp1lem6  23731  conpcon  23781  cvmliftmolem2  23828  cvmlift2lem12  23860  vdgr1d  23909  vdgr1b  23910  tfisg  24275  wfisg  24280  frinsg  24316  comppfsc  26410  fdc  26558  isbnd3  26611  vdioph  26962  fiphp3d  27005  dsmmfi  27307  frlmlbs  27352  symggen2  27515  psgnghm2  27541  matbas2  27578  phisum  27621  stirlinglem14  27939  pmap1N  30578  pol1N  30721  dia1N  31865  dihwN  32101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-rab 2565
  Copyright terms: Public domain W3C validator