Theorem spcv 3555

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  morex  3673  al0ssb  5241  rext  5384  relop  5785  dfpo2  6238  frxp  8051  frxp2  8069  findcard  9068  pssnn  9073  ssfi  9077  fiint  9206  marypha1lem  9312  dfom3  9532  elom3  9533  ttrclss  9605  aceq3lem  10006  dfac3  10007  dfac5lem4  10012  dfac5lem4OLD  10014  dfac8  10022  dfac9  10023  dfacacn  10028  dfac13  10029  kmlem1  10037  kmlem10  10046  fin23lem34  10232  fin23lem35  10233  zorn2lem7  10388  zornn0g  10391  axgroth6  10714  nnunb  12372  symggen  19377  gsumval3lem2  19813  gsumzaddlem  19828  dfac14  23528  i1fd  25604  chlimi  31206  ssdifidlprm  33415  zarclssn  33878  ddemeas  34241  onvf1odlem2  35140  dfon2lem4  35820  dfon2lem5  35821  dfon2lem7  35823  ttac  43069  dfac11  43095  dfac21  43099  nregmodel  45050  setrec2fun  49724