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

Theorem elabg 3196
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
Hypothesis
Ref Expression
elabg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elabg  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem elabg
StepHypRef Expression
1 nfcv 2564 . 2  |-  F/_ x A
2 nfv 1728 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 3193 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405    e. wcel 1842   {cab 2387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060
This theorem is referenced by:  elab2g  3197  intmin3  4255  elxpi  4838  finds  6709  wfrlem15  7034  elfi  7906  inficl  7918  dffi3  7924  scott0  8335  elgch  9029  nqpr  9421  hashf1lem1  12551  cshword  12816  trclublem  12976  cotrtrclfv  12993  dfiso2  15383  lubval  15936  glbval  15949  efgcpbllemb  17095  frgpuplem  17112  lspsn  17966  mpfind  18523  pf1ind  18709  eltg  19748  eltg2  19749  islocfin  20308  fbssfi  20628  elabreximd  27809  abfmpunirn  27919  orvcval  28888  islshpkrN  32118  setindtrs  35309  rngunsnply  35466  frege55lem1c  35877  nzss  36050  elabrexg  36786  afvelrnb  37597  afvelrnb0  37598  cshword2  37905
  Copyright terms: Public domain W3C validator