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

Theorem elab2g 2867
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 2866 . 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  2868  elab4g  2869  eldif  3104  elun  3258  elin  3300  elprg  3598  elsncg  3603  eluni  3771  eliun  3850  eliin  3851  elopab  4209  elong  4337  elrn2g  4823  eldmg  4827  elrnmpt  4879  elrnmpt1  4881  elimag  4969  elrnmpt2g  5855  eloprabi  6085  tfrlem12  6338  elqsg  6644  elixp2  6753  isacn  7604  isfin1a  7851  isfin2  7853  isfin4  7856  isfin7  7860  isfin3ds  7888  elwina  8241  elina  8242  iswun  8259  eltskg  8305  elgrug  8347  elnp  8544  elnpi  8545  iscat  13501  isps  14238  isdir  14281  elsymgbas2  14700  istopg  16568  isbasisg  16612  isufl  17535  2sqlem9  20539  isplig  20769  isgrpo  20788  isass  20908  isexid  20909  ismgm  20912  elghomlem2  20954  elunop  22377  adjeu  22394  dfon2lem3  23475  orderseqlem  23586  wfrlem15  23604  elno  23634  elaltxp  23849  isprsr  24556  iscom  24665  isptfin  25627  heiborlem1  25867  heiborlem10  25876
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 2742
  Copyright terms: Public domain W3C validator