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

Theorem elabg 3083
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 2572 . 2  |-  F/_ x A
2 nfv 1629 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 3080 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {cab 2422
This theorem is referenced by:  elab2g  3084  intmin3  4078  finds  4871  elxpi  4894  elfi  7418  inficl  7430  dffi3  7436  scott0  7810  elgch  8497  nqpr  8891  hashf1lem1  11704  efgcpbllemb  15387  frgpuplem  15404  lspsn  16078  eltg  17022  eltg2  17023  fbssfi  17869  mpfind  19965  pf1ind  19975  elabreximd  23991  abfmpunirn  24064  orvcval  24715  wfrlem15  25552  islocfin  26376  setindtrs  27096  rngunsnply  27355  afvelrnb  28003  afvelrnb0  28004  cshword  28235  islshpkrN  29918
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958
  Copyright terms: Public domain W3C validator