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

Theorem elab2g 3027
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 2451 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3026 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 249 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   {cab 2373
This theorem is referenced by:  elab2  3028  elab4g  3029  eldif  3273  elun  3431  elin  3473  elprg  3774  elsncg  3779  eluni  3960  eliun  4039  eliin  4040  elopab  4403  elong  4530  elrn2g  5001  eldmg  5005  elrnmpt  5057  elrnmpt1  5059  elimag  5147  elrnmpt2g  6121  eloprabi  6352  tfrlem12  6586  elqsg  6892  elixp2  7002  isacn  7858  isfin1a  8105  isfin2  8107  isfin4  8110  isfin7  8114  isfin3ds  8142  elwina  8494  elina  8495  iswun  8512  eltskg  8558  elgrug  8600  elnp  8797  elnpi  8798  iscat  13824  isps  14561  isdir  14604  elsymgbas2  15023  istopg  16891  isbasisg  16935  isufl  17866  isusp  18212  2sqlem9  21024  isplig  21613  isgrpo  21632  isass  21752  isexid  21753  ismgm  21756  elghomlem2  21798  elunop  23223  adjeu  23240  ballotlemfmpn  24531  dfon2lem3  25165  orderseqlem  25276  wfrlem15  25294  elno  25324  elaltxp  25534  isptfin  26066  heiborlem1  26211  heiborlem10  26220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901
  Copyright terms: Public domain W3C validator