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

Theorem elab2g 3252
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 2545 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3251 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 257 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115
This theorem is referenced by:  elab2  3253  elab4g  3254  eldif  3486  elun  3645  elin  3687  elprg  4043  elsncg  4050  eluni  4248  eliun  4330  eliin  4331  elopab  4755  elong  4886  elrn2g  5193  eldmg  5198  elrnmpt  5249  elrnmpt1  5251  elimag  5341  elrnmpt2g  6399  elrnmpt2res  6401  eloprabi  6847  tfrlem12  7059  elqsg  7364  elixp2  7474  isacn  8426  isfin1a  8673  isfin2  8675  isfin4  8678  isfin7  8682  isfin3ds  8710  elwina  9065  elina  9066  iswun  9083  eltskg  9129  elgrug  9171  elnp  9366  elnpi  9367  iscat  14930  isps  15692  isdir  15722  elsymgbas2  16220  mdetunilem9  18929  istopg  19211  isbasisg  19255  isptfin  19845  isufl  20241  isusp  20591  2sqlem9  23473  isplig  24952  isgrpo  24971  isass  25091  isexid  25092  ismgm  25095  elghomlem2  25137  elunop  26564  adjeu  26581  isarchi  27485  ispcmp  27613  eulerpartlemelr  28047  eulerpartlemgs2  28070  ballotlemfmpn  28184  ismfs  28660  dfon2lem3  29070  orderseqlem  29185  elno  29259  elaltxp  29478  heiborlem1  30137  heiborlem10  30146  nzss  31049  isuhgr  32060  isushgr  32061
  Copyright terms: Public domain W3C validator