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

Theorem rabid2 2821
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 2485 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
2 pm4.71 612 . . . 4  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  <->  ( x  e.  A  /\  ph )
) )
32albii 1572 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
41, 3bitr4i 244 . 2  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  ->  ph ) )
5 df-rab 2651 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2390 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2647 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
84, 6, 73bitr4i 269 1  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1717   {cab 2366   A.wral 2642   {crab 2646
This theorem is referenced by:  rabxm  3586  rabrsn  3810  iinrab2  4088  riinrab  4100  class2seteq  4302  dmmptg  5300  fneqeql  5770  fmpt  5822  zfrep6  5900  axdc2lem  8254  ioomax  10910  iccmax  10911  hashbc  11622  dfphi2  13083  phiprmpw  13085  isnsg4  14903  lssuni  15936  psr1baslem  16503  ocv0  16820  ordtrest2lem  17182  xkouni  17545  xkoccn  17565  tsmsfbas  18071  clsocv  19068  ovolicc2lem4  19276  itg2monolem1  19502  musum  20836  lgsquadlem2  20999  vdgr1d  21515  vdgr1b  21516  ubthlem1  22213  hasheuni  24264  measvuni  24355  imambfm  24399  subfacp1lem6  24643  conpcon  24694  cvmliftmolem2  24741  cvmlift2lem12  24773  tfisg  25221  wfisg  25226  frinsg  25262  comppfsc  26071  fdc  26133  isbnd3  26177  vdioph  26522  fiphp3d  26564  dsmmfi  26866  frlmlbs  26911  symggen2  27074  psgnghm2  27100  matbas2  27137  phisum  27180  stirlinglem14  27497  frgraregorufr0  27797  pmap1N  29932  pol1N  30075  dia1N  31219  dihwN  31455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-ral 2647  df-rab 2651
  Copyright terms: Public domain W3C validator