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

Theorem spcgv 3574
 Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2145, ax-11 2161. (Revised by Wolf Lammen, 25-Aug-2023.)
Hypothesis
Ref Expression
spcgv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcgv (𝐴𝑉 → (∀𝑥𝜑𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcgv
StepHypRef Expression
1 elex 3491 . 2 (𝐴𝑉𝐴 ∈ V)
2 id 22 . . 3 (𝐴 ∈ V → 𝐴 ∈ V)
3 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
43adantl 484 . . 3 ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑𝜓))
52, 4spcdv 3572 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
61, 5syl 17 1 (𝐴𝑉 → (∀𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   = wceq 1537   ∈ wcel 2114  Vcvv 3473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475 This theorem is referenced by:  spcv  3585  mob2  3686  intss1  4867  dfiin2g  4933  alxfr  5284  fri  5493  isofrlem  7070  tfisi  7551  limomss  7563  nnlim  7571  f1oweALT  7651  pssnn  8714  findcard3  8739  ttukeylem1  9909  rami  16329  ramcl  16343  islbs3  19903  mplsubglem  20190  mpllsslem  20191  uniopn  21481  chlimi  28996  dfon2lem3  33038  dfon2lem8  33043  neificl  35067  ismrcd1  39432  mnuop23d  40757
 Copyright terms: Public domain W3C validator