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

Theorem elab2g 2929
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 2360 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 2928 . 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 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  elab2  2930  elab4g  2931  eldif  3175  elun  3329  elin  3371  elprg  3670  elsncg  3675  eluni  3846  eliun  3925  eliin  3926  elopab  4288  elong  4416  elrn2g  4886  eldmg  4890  elrnmpt  4942  elrnmpt1  4944  elimag  5032  elrnmpt2g  5972  eloprabi  6202  tfrlem12  6421  elqsg  6727  elixp2  6836  isacn  7687  isfin1a  7934  isfin2  7936  isfin4  7939  isfin7  7943  isfin3ds  7971  elwina  8324  elina  8325  iswun  8342  eltskg  8388  elgrug  8430  elnp  8627  elnpi  8628  iscat  13590  isps  14327  isdir  14370  elsymgbas2  14789  istopg  16657  isbasisg  16701  isufl  17624  2sqlem9  20628  isplig  20860  isgrpo  20879  isass  20999  isexid  21000  ismgm  21003  elghomlem2  21045  elunop  22468  adjeu  22485  dfon2lem3  24212  orderseqlem  24323  wfrlem15  24341  elno  24371  elaltxp  24581  isprsr  25327  iscom  25436  isptfin  26398  heiborlem1  26638  heiborlem10  26647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator