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

Theorem spcgv 3143
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 2564 . 2  |-  F/_ x A
2 nfv 1728 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcgf 3138 1  |-  ( A  e.  V  ->  ( A. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1403    = wceq 1405    e. wcel 1842
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:  spcv  3149  mob2  3228  intss1  4241  dfiin2g  4303  alxfr  4603  fri  4784  isofrlem  6218  tfisi  6675  limomss  6687  nnlim  6695  f1oweALT  6767  pssnn  7772  findcard3  7796  ttukeylem1  8920  rami  14740  ramcl  14754  islbs3  18119  mplsubglem  18411  mpllsslem  18412  mplsubglemOLD  18413  mpllsslemOLD  18414  uniopn  19696  0eusgraiff0rgra  25343  chlimi  26552  dfon2lem3  29991  dfon2lem8  29996  neificl  31508  ismrcd1  34972
  Copyright terms: Public domain W3C validator