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

Theorem spcgv 3324
 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:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcgv
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
2 nfv 1883 . 2 𝑥𝜓
3 spcgv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3spcgf 3319 1 (𝐴𝑉 → (∀𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521   = wceq 1523   ∈ wcel 2030 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233 This theorem is referenced by:  spcv  3330  mob2  3419  intss1  4524  dfiin2g  4585  alxfr  4908  fri  5105  isofrlem  6630  tfisi  7100  limomss  7112  nnlim  7120  f1oweALT  7194  pssnn  8219  findcard3  8244  ttukeylem1  9369  rami  15766  ramcl  15780  islbs3  19203  mplsubglem  19482  mpllsslem  19483  uniopn  20750  chlimi  28219  dfon2lem3  31814  dfon2lem8  31819  neificl  33679  ismrcd1  37578
 Copyright terms: Public domain W3C validator