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

Theorem elab2g 3186
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 2520 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3185 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 261 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1443    e. wcel 1886   {cab 2436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046
This theorem is referenced by:  elab2  3187  elab4g  3188  eldif  3413  elun  3573  elin  3616  elprg  3983  elsncg  3990  eluni  4200  eliun  4282  eliin  4283  elopab  4708  elrn2g  5024  eldmg  5029  elrnmpt  5080  elrnmpt1  5082  elimag  5171  elong  5430  elrnmpt2g  6405  elrnmpt2res  6407  eloprabi  6852  tfrlem12  7104  elqsg  7412  elixp2  7523  isacn  8472  isfin1a  8719  isfin2  8721  isfin4  8724  isfin7  8728  isfin3ds  8756  elwina  9108  elina  9109  iswun  9126  eltskg  9172  elgrug  9214  elnp  9409  elnpi  9410  iscat  15571  isps  16441  isdir  16471  ismgm  16482  elsymgbas2  17015  mdetunilem9  19638  istopg  19918  isbasisg  19955  isptfin  20524  isufl  20921  isusp  21269  2sqlem9  24294  isplig  25902  isgrpo  25917  isass  26037  isexid  26038  ismgmOLD  26041  elghomlem2OLD  26083  elunop  27518  adjeu  27535  isarchi  28492  ispcmp  28677  eulerpartlemelr  29183  eulerpartlemgs2  29206  ballotlemfmpn  29320  ismfs  30180  dfon2lem3  30424  orderseqlem  30483  elno  30526  elaltxp  30735  heiborlem1  32136  heiborlem10  32145  nzss  36660  elrnmptf  37448  issal  38169  isuhgr  39137  isushgr  39138  isupgr  39162  isumgr  39171  isuspgr  39225  isusgr  39226  iscplgr  39465  isuhgrALTV  39665  isushgrALTV  39666  ismgmALT  39846
  Copyright terms: Public domain W3C validator