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

Theorem spcgv 2944
Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)
Hypothesis
Ref Expression
spcgv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spcgv  |-  ( A  e.  V  ->  ( A. x ph  ->  ps ) )
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem spcgv
StepHypRef Expression
1 nfcv 2494 . 2  |-  F/_ x A
2 nfv 1619 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcgf 2939 1  |-  ( A  e.  V  ->  ( A. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1540    = wceq 1642    e. wcel 1710
This theorem is referenced by:  spcv  2950  mob2  3021  intss1  3956  dfiin2g  4015  fri  4434  alxfr  4626  tfisi  4728  limomss  4740  nnlim  4748  isofrlem  5921  f1oweALT  5935  pssnn  7166  findcard3  7187  ttukeylem1  8223  rami  13153  ramcl  13167  clatlem  14309  islbs3  16001  mplsubglem  16272  mpllsslem  16273  uniopn  16743  chlimi  21922  relexpind  24441  dfon2lem3  24699  dfon2lem8  24704  neificl  25791  ismrcd1  26096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866
  Copyright terms: Public domain W3C validator