Theorem spcv 3589

Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)

Hypotheses

Ref	Expression
spcv.1	⊢ 𝐴 ∈ V
spcv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcv	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcv

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcgv 3580	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   = wceq 1539   ∈ wcel 2107  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466

This theorem is referenced by:  morex  3709  al0ssb  5290  rext  5435  relop  5843  dfpo2  6298  frxp  8134  frxp2  8152  findcard  9186  pssnn  9191  ssfi  9196  fiint  9349  fiintOLD  9350  marypha1lem  9456  dfom3  9670  elom3  9671  ttrclss  9743  aceq3lem  10143  dfac3  10144  dfac5lem4  10149  dfac5lem4OLD  10151  dfac8  10159  dfac9  10160  dfacacn  10165  dfac13  10166  kmlem1  10174  kmlem10  10183  fin23lem34  10369  fin23lem35  10370  zorn2lem7  10525  zornn0g  10528  axgroth6  10851  nnunb  12506  symggen  19461  gsumval3lem2  19897  gsumzaddlem  19912  dfac14  23591  i1fd  25671  chlimi  31200  ssdifidlprm  33427  zarclssn  33813  ddemeas  34178  dfon2lem4  35728  dfon2lem5  35729  dfon2lem7  35731  ttac  42993  dfac11  43019  dfac21  43023  setrec2fun  49207