Theorem spcv 3548

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  morex  3666  al0ssb  5243  rext  5395  relop  5799  dfpo2  6254  frxp  8069  frxp2  8087  findcard  9091  pssnn  9096  ssfi  9100  fiint  9230  marypha1lem  9339  dfom3  9559  elom3  9560  ttrclss  9632  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  10742  nnunb  12424  symggen  19436  gsumval3lem2  19872  gsumzaddlem  19887  dfac14  23593  i1fd  25658  chlimi  31320  ssdifidlprm  33533  zarclssn  34033  ddemeas  34396  onvf1odlem2  35302  dfon2lem4  35982  dfon2lem5  35983  dfon2lem7  35985  ttac  43482  dfac11  43508  dfac21  43512  nregmodel  45462  setrec2fun  50179