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

Theorem spcgv 3155
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 2613 . 2  |-  F/_ x A
2 nfv 1674 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcgf 3150 1  |-  ( A  e.  V  ->  ( A. x ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072
This theorem is referenced by:  spcv  3161  mob2  3238  intss1  4243  dfiin2g  4303  alxfr  4605  fri  4782  isofrlem  6132  tfisi  6571  limomss  6583  nnlim  6591  f1oweALT  6663  pssnn  7634  findcard3  7658  ttukeylem1  8781  rami  14180  ramcl  14194  islbs3  17344  mplsubglem  17619  mpllsslem  17620  mplsubglemOLD  17621  mpllsslemOLD  17622  uniopn  18628  chlimi  24774  relexpind  27478  dfon2lem3  27734  dfon2lem8  27739  neificl  28789  ismrcd1  29174
  Copyright terms: Public domain W3C validator