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

Theorem elab2g 2918
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elab2g.2  |-  B  =  { x  |  ph }
Assertion
Ref Expression
elab2g  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    B( x)    V( x)

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3  |-  B  =  { x  |  ph }
21eleq2i 2349 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 2917 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 250 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1624    e. wcel 1685   {cab 2271
This theorem is referenced by:  elab2  2919  elab4g  2920  eldif  3164  elun  3318  elin  3360  elprg  3659  elsncg  3664  eluni  3832  eliun  3911  eliin  3912  elopab  4272  elong  4400  elrn2g  4870  eldmg  4874  elrnmpt  4926  elrnmpt1  4928  elimag  5016  elrnmpt2g  5918  eloprabi  6148  tfrlem12  6401  elqsg  6707  elixp2  6816  isacn  7667  isfin1a  7914  isfin2  7916  isfin4  7919  isfin7  7923  isfin3ds  7951  elwina  8304  elina  8305  iswun  8322  eltskg  8368  elgrug  8410  elnp  8607  elnpi  8608  iscat  13569  isps  14306  isdir  14349  elsymgbas2  14768  istopg  16636  isbasisg  16680  isufl  17603  2sqlem9  20607  isplig  20837  isgrpo  20856  isass  20976  isexid  20977  ismgm  20980  elghomlem2  21022  elunop  22445  adjeu  22462  dfon2lem3  23543  orderseqlem  23654  wfrlem15  23672  elno  23702  elaltxp  23917  isprsr  24624  iscom  24733  isptfin  25695  heiborlem1  25935  heiborlem10  25944
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792
  Copyright terms: Public domain W3C validator