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

Theorem elab2g 2884
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 2320 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 2883 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 250 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2242
This theorem is referenced by:  elab2  2885  elab4g  2886  eldif  3123  elun  3277  elin  3319  elprg  3617  elsncg  3622  eluni  3790  eliun  3869  eliin  3870  elopab  4230  elong  4358  elrn2g  4844  eldmg  4848  elrnmpt  4900  elrnmpt1  4902  elimag  4990  elrnmpt2g  5876  eloprabi  6106  tfrlem12  6359  elqsg  6665  elixp2  6774  isacn  7625  isfin1a  7872  isfin2  7874  isfin4  7877  isfin7  7881  isfin3ds  7909  elwina  8262  elina  8263  iswun  8280  eltskg  8326  elgrug  8368  elnp  8565  elnpi  8566  iscat  13522  isps  14259  isdir  14302  elsymgbas2  14721  istopg  16589  isbasisg  16633  isufl  17556  2sqlem9  20560  isplig  20790  isgrpo  20809  isass  20929  isexid  20930  ismgm  20933  elghomlem2  20975  elunop  22398  adjeu  22415  dfon2lem3  23496  orderseqlem  23607  wfrlem15  23625  elno  23655  elaltxp  23870  isprsr  24577  iscom  24686  isptfin  25648  heiborlem1  25888  heiborlem10  25897
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759
  Copyright terms: Public domain W3C validator