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

Theorem elab2g 3090
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 2506 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3089 . 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 4    <-> wb 178    = wceq 1653    e. wcel 1727   {cab 2428
This theorem is referenced by:  elab2  3091  elab4g  3092  eldif  3316  elun  3474  elin  3516  elprg  3855  elsncg  3860  eluni  4042  eliun  4121  eliin  4122  elopab  4491  elong  4618  elrn2g  5090  eldmg  5094  elrnmpt  5146  elrnmpt1  5148  elimag  5236  elrnmpt2g  6211  eloprabi  6442  tfrlem12  6679  elqsg  6985  elixp2  7095  isacn  7956  isfin1a  8203  isfin2  8205  isfin4  8208  isfin7  8212  isfin3ds  8240  elwina  8592  elina  8593  iswun  8610  eltskg  8656  elgrug  8698  elnp  8895  elnpi  8896  iscat  13928  isps  14665  isdir  14708  elsymgbas2  15127  istopg  16999  isbasisg  17043  isufl  17976  isusp  18322  2sqlem9  21188  isplig  21796  isgrpo  21815  isass  21935  isexid  21936  ismgm  21939  elghomlem2  21981  elunop  23406  adjeu  23423  ballotlemfmpn  24783  dfon2lem3  25443  orderseqlem  25558  elno  25632  elaltxp  25851  isptfin  26413  heiborlem1  26558  heiborlem10  26567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964
  Copyright terms: Public domain W3C validator