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

Theorem rabid2 2910
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 2551 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
2 pm4.71 630 . . . 4  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  <->  ( x  e.  A  /\  ph )
) )
32albii 1610 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  ph ) ) )
41, 3bitr4i 252 . 2  |-  ( A  =  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  A  ->  ph ) )
5 df-rab 2736 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
65eqeq2i 2453 . 2  |-  ( A  =  { x  e.  A  |  ph }  <->  A  =  { x  |  ( x  e.  A  /\  ph ) } )
7 df-ral 2732 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
84, 6, 73bitr4i 277 1  |-  ( A  =  { x  e.  A  |  ph }  <->  A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2727   {crab 2731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2732  df-rab 2736
This theorem is referenced by:  rabxm  3672  iinrab2  4245  riinrab  4258  class2seteq  4472  dmmptg  5347  fneqeql  5823  fmpt  5876  zfrep6  6557  axdc2lem  8629  ioomax  11382  iccmax  11383  hashbc  12218  dfphi2  13861  phiprmpw  13863  isnsg4  15736  symggen2  15989  psgnfvalfi  16031  lssuni  17033  psr1baslem  17653  psgnghm2  18023  ocv0  18114  dsmmfi  18175  frlmfibas  18201  frlmlbs  18237  ordtrest2lem  18819  xkouni  19184  xkoccn  19204  tsmsfbas  19710  clsocv  20774  ehlbase  20922  ovolicc2lem4  21015  itg2monolem1  21240  musum  22543  lgsquadlem2  22706  vdgr1d  23585  vdgr1b  23586  ubthlem1  24283  xrsclat  26153  ordtrest2NEWlem  26364  hasheuni  26546  measvuni  26640  ddemeas  26664  imambfm  26689  subfacp1lem6  27085  conpcon  27136  cvmliftmolem2  27183  cvmlift2lem12  27215  tfisg  27677  wfisg  27682  frinsg  27718  comppfsc  28591  fdc  28653  isbnd3  28695  vdioph  29130  fiphp3d  29170  phisum  29579  stirlinglem14  29894  frgraregorufr0  30657  pmap1N  33423  pol1N  33566  dia1N  34710  dihwN  34946
  Copyright terms: Public domain W3C validator