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

Theorem elab2g 3232
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 2519 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3231 . 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 1381    e. wcel 1802   {cab 2426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095
This theorem is referenced by:  elab2  3233  elab4g  3234  eldif  3468  elun  3627  elin  3669  elprg  4026  elsncg  4033  eluni  4233  eliun  4316  eliin  4317  elopab  4741  elong  4872  elrn2g  5179  eldmg  5184  elrnmpt  5235  elrnmpt1  5237  elimag  5327  elrnmpt2g  6395  elrnmpt2res  6397  eloprabi  6843  tfrlem12  7056  elqsg  7361  elixp2  7471  isacn  8423  isfin1a  8670  isfin2  8672  isfin4  8675  isfin7  8679  isfin3ds  8707  elwina  9062  elina  9063  iswun  9080  eltskg  9126  elgrug  9168  elnp  9363  elnpi  9364  iscat  14941  isps  15701  isdir  15731  ismgm  15742  elsymgbas2  16275  mdetunilem9  18989  istopg  19271  isbasisg  19315  isptfin  19883  isufl  20280  isusp  20630  2sqlem9  23513  isplig  25044  isgrpo  25063  isass  25183  isexid  25184  ismgmOLD  25187  elghomlem2OLD  25229  elunop  26656  adjeu  26673  isarchi  27592  ispcmp  27726  eulerpartlemelr  28162  eulerpartlemgs2  28185  ballotlemfmpn  28299  ismfs  28775  dfon2lem3  29185  orderseqlem  29300  elno  29374  elaltxp  29593  heiborlem1  30275  heiborlem10  30284  nzss  31191  isuhgr  32200  isushgr  32201  ismgmALT  32380
  Copyright terms: Public domain W3C validator