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

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
StepHypRef Expression
1 nfcv 2619 . 2
2 nfv 1707 . 2
3 spcgv.1 . 2
41, 2, 3spcgf 3189 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator