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

Theorem elab2g 2853
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 2317 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 2852 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 250 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2239
This theorem is referenced by:  elab2  2854  elab4g  2855  eldif  3088  elun  3226  elin  3266  elprg  3561  elsncg  3566  eluni  3730  eliun  3807  eliin  3808  elopab  4165  elong  4293  elrn2g  4777  eldmg  4781  elrnmpt  4833  elrnmpt1  4835  elimag  4923  elrnmpt2g  5808  eloprabi  6038  tfrlem12  6291  elqsg  6597  elixp2  6706  isacn  7555  isfin1a  7802  isfin2  7804  isfin4  7807  isfin7  7811  isfin3ds  7839  elwina  8188  elina  8189  iswun  8206  eltskg  8252  elgrug  8294  elnp  8491  elnpi  8492  iscat  13418  isps  14146  isdir  14189  elsymgbas2  14608  istopg  16473  isbasisg  16517  isufl  17440  2sqlem9  20444  isplig  20674  isgrpo  20693  isass  20813  isexid  20814  ismgm  20817  elghomlem2  20859  elunop  22282  adjeu  22299  dfon2lem3  23309  orderseqlem  23420  wfrlem15  23438  elno  23468  elaltxp  23683  isprsr  24390  iscom  24499  isptfin  25461  heiborlem1  25701  heiborlem10  25710
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729
  Copyright terms: Public domain W3C validator