Theorem spcv 3562

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109  Vcvv 3438

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440

This theorem is referenced by:  morex  3681  al0ssb  5250  rext  5395  relop  5797  dfpo2  6248  frxp  8066  frxp2  8084  findcard  9087  pssnn  9092  ssfi  9097  fiint  9235  fiintOLD  9236  marypha1lem  9342  dfom3  9562  elom3  9563  ttrclss  9635  aceq3lem  10033  dfac3  10034  dfac5lem4  10039  dfac5lem4OLD  10041  dfac8  10049  dfac9  10050  dfacacn  10055  dfac13  10056  kmlem1  10064  kmlem10  10073  fin23lem34  10259  fin23lem35  10260  zorn2lem7  10415  zornn0g  10418  axgroth6  10741  nnunb  12398  symggen  19367  gsumval3lem2  19803  gsumzaddlem  19818  dfac14  23521  i1fd  25598  chlimi  31196  ssdifidlprm  33408  zarclssn  33842  ddemeas  34205  onvf1odlem2  35079  dfon2lem4  35762  dfon2lem5  35763  dfon2lem7  35765  ttac  43012  dfac11  43038  dfac21  43042  nregmodel  44994  setrec2fun  49681