Theorem spcv 3618

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 3609	. 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  morex  3741  al0ssb  5326  rext  5468  relop  5875  dfpo2  6327  frxp  8167  frxp2  8185  findcard  9229  pssnn  9234  ssfi  9240  fiint  9394  fiintOLD  9395  marypha1lem  9502  dfom3  9716  elom3  9717  ttrclss  9789  aceq3lem  10189  dfac3  10190  dfac5lem4  10195  dfac5lem4OLD  10197  dfac8  10205  dfac9  10206  dfacacn  10211  dfac13  10212  kmlem1  10220  kmlem10  10229  fin23lem34  10415  fin23lem35  10416  zorn2lem7  10571  zornn0g  10574  axgroth6  10897  nnunb  12549  symggen  19512  gsumval3lem2  19948  gsumzaddlem  19963  dfac14  23647  i1fd  25735  chlimi  31266  ssdifidlprm  33451  zarclssn  33819  ddemeas  34200  dfon2lem4  35750  dfon2lem5  35751  dfon2lem7  35753  ttac  42993  dfac11  43019  dfac21  43023  setrec2fun  48784