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

Theorem rabid2 2877
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 2540 . . 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 1575 . . 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 2706 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2445 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2702 . 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 1549    = wceq 1652    e. wcel 1725   {cab 2421   A.wral 2697   {crab 2701
This theorem is referenced by:  rabxm  3642  rabrsn  3866  iinrab2  4146  riinrab  4158  class2seteq  4360  dmmptg  5359  fneqeql  5830  fmpt  5882  zfrep6  5960  axdc2lem  8320  ioomax  10977  iccmax  10978  hashbc  11694  dfphi2  13155  phiprmpw  13157  isnsg4  14975  lssuni  16008  psr1baslem  16575  ocv0  16896  ordtrest2lem  17259  xkouni  17623  xkoccn  17643  tsmsfbas  18149  clsocv  19196  ovolicc2lem4  19408  itg2monolem1  19634  musum  20968  lgsquadlem2  21131  vdgr1d  21666  vdgr1b  21667  ubthlem1  22364  hasheuni  24467  measvuni  24560  imambfm  24604  subfacp1lem6  24863  conpcon  24914  cvmliftmolem2  24961  cvmlift2lem12  24993  tfisg  25471  wfisg  25476  frinsg  25512  comppfsc  26378  fdc  26440  isbnd3  26484  vdioph  26829  fiphp3d  26871  dsmmfi  27172  frlmlbs  27217  symggen2  27380  psgnghm2  27406  matbas2  27443  phisum  27486  stirlinglem14  27803  frgraregorufr0  28378  pmap1N  30501  pol1N  30644  dia1N  31788  dihwN  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-rab 2706
  Copyright terms: Public domain W3C validator