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

Theorem rabid2 2887
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 2543 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
2 pm4.71 613 . . . 4  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  <->  ( x  e.  A  /\  ph )
) )
32albii 1576 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
41, 3bitr4i 245 . 2  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  ->  ph ) )
5 df-rab 2716 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2448 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2712 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
84, 6, 73bitr4i 270 1  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   A.wal 1550    = wceq 1653    e. wcel 1726   {cab 2424   A.wral 2707   {crab 2711
This theorem is referenced by:  rabxm  3652  rabrsn  3876  iinrab2  4156  riinrab  4169  class2seteq  4371  dmmptg  5370  fneqeql  5841  fmpt  5893  zfrep6  5971  axdc2lem  8333  ioomax  10990  iccmax  10991  hashbc  11707  dfphi2  13168  phiprmpw  13170  isnsg4  14988  lssuni  16021  psr1baslem  16588  ocv0  16909  ordtrest2lem  17272  xkouni  17636  xkoccn  17656  tsmsfbas  18162  clsocv  19209  ovolicc2lem4  19421  itg2monolem1  19645  musum  20981  lgsquadlem2  21144  vdgr1d  21679  vdgr1b  21680  ubthlem1  22377  hasheuni  24480  measvuni  24573  imambfm  24617  subfacp1lem6  24876  conpcon  24927  cvmliftmolem2  24974  cvmlift2lem12  25006  tfisg  25484  wfisg  25489  frinsg  25525  comppfsc  26401  fdc  26463  isbnd3  26507  vdioph  26852  fiphp3d  26894  dsmmfi  27195  frlmlbs  27240  symggen2  27403  psgnghm2  27429  matbas2  27466  phisum  27509  stirlinglem14  27826  frgraregorufr0  28515  pmap1N  30638  pol1N  30781  dia1N  31925  dihwN  32161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-rab 2716
  Copyright terms: Public domain W3C validator