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

Theorem elab2g 3071
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 2494 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3070 . 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 1652    e. wcel 1725   {cab 2416
This theorem is referenced by:  elab2  3072  elab4g  3073  eldif  3317  elun  3475  elin  3517  elprg  3818  elsncg  3823  eluni  4005  eliun  4084  eliin  4085  elopab  4449  elong  4576  elrn2g  5047  eldmg  5051  elrnmpt  5103  elrnmpt1  5105  elimag  5193  elrnmpt2g  6168  eloprabi  6399  tfrlem12  6636  elqsg  6942  elixp2  7052  isacn  7909  isfin1a  8156  isfin2  8158  isfin4  8161  isfin7  8165  isfin3ds  8193  elwina  8545  elina  8546  iswun  8563  eltskg  8609  elgrug  8651  elnp  8848  elnpi  8849  iscat  13880  isps  14617  isdir  14660  elsymgbas2  15079  istopg  16951  isbasisg  16995  isufl  17928  isusp  18274  2sqlem9  21140  isplig  21748  isgrpo  21767  isass  21887  isexid  21888  ismgm  21891  elghomlem2  21933  elunop  23358  adjeu  23375  ballotlemfmpn  24735  dfon2lem3  25391  orderseqlem  25502  wfrlem15  25520  elno  25550  elaltxp  25763  isptfin  26307  heiborlem1  26452  heiborlem10  26461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945
  Copyright terms: Public domain W3C validator