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

Theorem elabg 2928
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 2432 . 2  |-  F/_ x A
2 nfv 1609 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 2925 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  elab2g  2929  intmin3  3906  finds  4698  elxpi  4721  elfi  7183  inficl  7194  dffi3  7200  scott0  7572  elgch  8260  nqpr  8654  hashf1lem1  11409  efgcpbllemb  15080  frgpuplem  15097  lspsn  15775  eltg  16711  eltg2  16712  fbssfi  17548  mpfind  19444  pf1ind  19454  elabreximd  23055  ballotlemfmpn  23069  abfmpunirn  23231  orvcval  23673  eloi  25189  elixp2b  25257  domrancur1b  25303  domrancur1c  25305  isoriso2  25316  isdir2  25395  intopcoaconlem3b  25641  iscol2  26196  islocfin  26399  setindtrs  27221  rngunsnply  27481  afvelrnb  28131  afvelrnb0  28132  islshpkrN  29932
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator