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

Theorem elab2g 3217
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 2498 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3216 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 260 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1867   {cab 2405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080
This theorem is referenced by:  elab2  3218  elab4g  3219  eldif  3443  elun  3603  elin  3646  elprg  4009  elsncg  4016  eluni  4216  eliun  4298  eliin  4299  elopab  4720  elrn2g  5036  eldmg  5041  elrnmpt  5092  elrnmpt1  5094  elimag  5183  elong  5441  elrnmpt2g  6413  elrnmpt2res  6415  eloprabi  6860  tfrlem12  7106  elqsg  7414  elixp2  7525  isacn  8464  isfin1a  8711  isfin2  8713  isfin4  8716  isfin7  8720  isfin3ds  8748  elwina  9100  elina  9101  iswun  9118  eltskg  9164  elgrug  9206  elnp  9401  elnpi  9402  iscat  15530  isps  16400  isdir  16430  ismgm  16441  elsymgbas2  16974  mdetunilem9  19582  istopg  19862  isbasisg  19899  isptfin  20468  isufl  20865  isusp  21213  2sqlem9  24203  isplig  25795  isgrpo  25810  isass  25930  isexid  25931  ismgmOLD  25934  elghomlem2OLD  25976  elunop  27401  adjeu  27418  isarchi  28378  ispcmp  28564  eulerpartlemelr  29057  eulerpartlemgs2  29080  ballotlemfmpn  29194  ismfs  30016  dfon2lem3  30259  orderseqlem  30318  elno  30361  elaltxp  30568  heiborlem1  31891  heiborlem10  31900  nzss  36351  elrnmptf  37125  issal  37770  isuhgr  38493  isushgr  38494  ismgmALT  38674
  Copyright terms: Public domain W3C validator