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 2141, ax-11 2157. (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 3501 . 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 1538   = wceq 1540  wcel 2108  Vcvv 3480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482
This theorem is referenced by:  spcv  3605  mob2  3721  sbceqal  3851  intss1  4963  dfiin2g  5032  alxfr  5407  friOLD  5643  funmo  6581  isofrlem  7360  tfisi  7880  limomss  7892  nnlim  7901  f1oweALT  7997  pssnn  9208  findcard3  9318  findcard3OLD  9319  frmin  9789  ttukeylem1  10549  rami  17053  ramcl  17067  islbs3  21157  mplsubglem  22019  mpllsslem  22020  uniopn  22903  chlimi  31253  iinabrex  32582  dfon2lem3  35786  dfon2lem8  35791  neificl  37760  hashnexinj  42129  ismrcd1  42709  mnuop23d  44285  relpfrlem  44974  modelaxreplem2  44996
  Copyright terms: Public domain W3C validator