Theorem spcgv 3194

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

Assertion

Ref	Expression
spcgv

Distinct variable groups:   ,   ,

Proof of Theorem spcgv

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2
2		nfv 1707	. 2
3		spcgv.1	. 2
4	1, 2, 3	spcgf 3189	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818

This theorem is referenced by:  spcv  3200  mob2  3279  intss1  4301  dfiin2g  4363  alxfr  4665  fri  4846  isofrlem  6236  tfisi  6693  limomss  6705  nnlim  6713  f1oweALT  6784  pssnn  7758  findcard3  7783  ttukeylem1  8910  rami  14533  ramcl  14547  islbs3  17801  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  uniopn  19406  0eusgraiff0rgra  24939  chlimi  26152  relexpind  29063  dfon2lem3  29217  dfon2lem8  29222  neificl  30246  ismrcd1  30630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111