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

Theorem spcgv 3596
Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2139, ax-11 2155. (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 3499 . 2 (𝐴𝑉𝐴 ∈ V)
2 id 22 . . 3 (𝐴 ∈ V → 𝐴 ∈ V)
3 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
43adantl 481 . . 3 ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑𝜓))
52, 4spcdv 3594 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
61, 5syl 17 1 (𝐴𝑉 → (∀𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535   = wceq 1537  wcel 2106  Vcvv 3478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480
This theorem is referenced by:  spcv  3605  mob2  3724  sbceqal  3857  intss1  4968  dfiin2g  5037  alxfr  5413  friOLD  5647  funmo  6583  isofrlem  7360  tfisi  7880  limomss  7892  nnlim  7901  f1oweALT  7996  pssnn  9207  findcard3  9316  findcard3OLD  9317  frmin  9787  ttukeylem1  10547  rami  17049  ramcl  17063  islbs3  21175  mplsubglem  22037  mpllsslem  22038  uniopn  22919  chlimi  31263  iinabrex  32589  dfon2lem3  35767  dfon2lem8  35772  neificl  37740  hashnexinj  42110  ismrcd1  42686  mnuop23d  44262  modelaxreplem2  44944
  Copyright terms: Public domain W3C validator