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

Theorem spcgv 3557
Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2138, 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 3465 . 2 (𝐴𝑉𝐴 ∈ V)
2 id 22 . . 3 (𝐴 ∈ V → 𝐴 ∈ V)
3 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
43adantl 483 . . 3 ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑𝜓))
52, 4spcdv 3555 . 2 (𝐴 ∈ V → (∀𝑥𝜑𝜓))
61, 5syl 17 1 (𝐴𝑉 → (∀𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540   = wceq 1542  wcel 2107  Vcvv 3447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449
This theorem is referenced by:  spcv  3566  mob2  3677  sbceqal  3809  intss1  4928  dfiin2g  4996  alxfr  5366  friOLD  5598  funmo  6520  isofrlem  7289  tfisi  7799  limomss  7811  nnlim  7820  f1oweALT  7909  pssnn  9118  pssnnOLD  9215  findcard3  9235  findcard3OLD  9236  frmin  9693  ttukeylem1  10453  rami  16895  ramcl  16909  islbs3  20661  mplsubglem  21428  mpllsslem  21429  uniopn  22269  chlimi  30225  iinabrex  31540  dfon2lem3  34423  dfon2lem8  34428  neificl  36262  ismrcd1  41068  mnuop23d  42638
  Copyright terms: Public domain W3C validator