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

Theorem spcgv 3198
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 2629 . 2  |-  F/_ x A
2 nfv 1683 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcgf 3193 1  |-  ( A  e.  V  ->  ( A. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115
This theorem is referenced by:  spcv  3204  mob2  3283  intss1  4297  dfiin2g  4358  alxfr  4660  fri  4841  isofrlem  6222  tfisi  6671  limomss  6683  nnlim  6691  f1oweALT  6765  pssnn  7735  findcard3  7759  ttukeylem1  8885  rami  14388  ramcl  14402  islbs3  17584  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  uniopn  19173  chlimi  25828  relexpind  28538  dfon2lem3  28794  dfon2lem8  28799  neificl  29849  ismrcd1  30234
  Copyright terms: Public domain W3C validator