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

Theorem spcgv 3587
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 3493 . 2 (𝐴𝑉𝐴 ∈ V)
2 id 22 . . 3 (𝐴 ∈ V → 𝐴 ∈ V)
3 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
43adantl 483 . . 3 ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑𝜓))
52, 4spcdv 3585 . 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 3475
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 3477
This theorem is referenced by:  spcv  3596  mob2  3712  sbceqal  3844  intss1  4968  dfiin2g  5036  alxfr  5406  friOLD  5638  funmo  6564  isofrlem  7337  tfisi  7848  limomss  7860  nnlim  7869  f1oweALT  7959  pssnn  9168  pssnnOLD  9265  findcard3  9285  findcard3OLD  9286  frmin  9744  ttukeylem1  10504  rami  16948  ramcl  16962  islbs3  20768  mplsubglem  21558  mpllsslem  21559  uniopn  22399  chlimi  30518  iinabrex  31831  dfon2lem3  34788  dfon2lem8  34793  neificl  36669  ismrcd1  41484  mnuop23d  43073
  Copyright terms: Public domain W3C validator