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

Theorem elab2g 3044
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 2468 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3043 . 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 1721   {cab 2390
This theorem is referenced by:  elab2  3045  elab4g  3046  eldif  3290  elun  3448  elin  3490  elprg  3791  elsncg  3796  eluni  3978  eliun  4057  eliin  4058  elopab  4422  elong  4549  elrn2g  5020  eldmg  5024  elrnmpt  5076  elrnmpt1  5078  elimag  5166  elrnmpt2g  6141  eloprabi  6372  tfrlem12  6609  elqsg  6915  elixp2  7025  isacn  7881  isfin1a  8128  isfin2  8130  isfin4  8133  isfin7  8137  isfin3ds  8165  elwina  8517  elina  8518  iswun  8535  eltskg  8581  elgrug  8623  elnp  8820  elnpi  8821  iscat  13852  isps  14589  isdir  14632  elsymgbas2  15051  istopg  16923  isbasisg  16967  isufl  17898  isusp  18244  2sqlem9  21110  isplig  21718  isgrpo  21737  isass  21857  isexid  21858  ismgm  21861  elghomlem2  21903  elunop  23328  adjeu  23345  ballotlemfmpn  24705  dfon2lem3  25355  orderseqlem  25466  wfrlem15  25484  elno  25514  elaltxp  25724  isptfin  26265  heiborlem1  26410  heiborlem10  26419
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918
  Copyright terms: Public domain W3C validator