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

Theorem elab2g 3215
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 2532 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3214 . 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 1370    e. wcel 1758   {cab 2439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080
This theorem is referenced by:  elab2  3216  elab4g  3217  eldif  3449  elun  3608  elin  3650  elprg  4004  elsncg  4011  eluni  4205  eliun  4286  eliin  4287  elopab  4708  elong  4838  elrn2g  5141  eldmg  5146  elrnmpt  5197  elrnmpt1  5199  elimag  5284  elrnmpt2g  6315  elrnmpt2res  6317  eloprabi  6749  tfrlem12  6961  elqsg  7265  elixp2  7380  isacn  8328  isfin1a  8575  isfin2  8577  isfin4  8580  isfin7  8584  isfin3ds  8612  elwina  8967  elina  8968  iswun  8985  eltskg  9031  elgrug  9073  elnp  9270  elnpi  9271  iscat  14732  isps  15494  isdir  15524  elsymgbas2  16008  mdetunilem9  18561  istopg  18643  isbasisg  18687  isufl  19621  isusp  19971  2sqlem9  22848  isplig  23836  isgrpo  23855  isass  23975  isexid  23976  ismgm  23979  elghomlem2  24021  elunop  25448  adjeu  25465  isarchi  26364  eulerpartlemelr  26904  eulerpartlemgs2  26927  ballotlemfmpn  27041  dfon2lem3  27762  orderseqlem  27877  elno  27951  elaltxp  28170  isptfin  28735  heiborlem1  28878  heiborlem10  28887
  Copyright terms: Public domain W3C validator