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

Theorem elab2g 2916
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 2347 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 2915 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 248 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  elab2  2917  elab4g  2918  eldif  3162  elun  3316  elin  3358  elprg  3657  elsncg  3662  eluni  3830  eliun  3909  eliin  3910  elopab  4272  elong  4400  elrn2g  4870  eldmg  4874  elrnmpt  4926  elrnmpt1  4928  elimag  5016  elrnmpt2g  5956  eloprabi  6186  tfrlem12  6405  elqsg  6711  elixp2  6820  isacn  7671  isfin1a  7918  isfin2  7920  isfin4  7923  isfin7  7927  isfin3ds  7955  elwina  8308  elina  8309  iswun  8326  eltskg  8372  elgrug  8414  elnp  8611  elnpi  8612  iscat  13574  isps  14311  isdir  14354  elsymgbas2  14773  istopg  16641  isbasisg  16685  isufl  17608  2sqlem9  20612  isplig  20844  isgrpo  20863  isass  20983  isexid  20984  ismgm  20987  elghomlem2  21029  elunop  22452  adjeu  22469  dfon2lem3  24141  orderseqlem  24252  wfrlem15  24270  elno  24300  elaltxp  24509  isprsr  25224  iscom  25333  isptfin  26295  heiborlem1  26535  heiborlem10  26544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator