Theorem spcv 3547

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  morex  3665  al0ssb  5243  rext  5400  relop  5805  dfpo2  6260  frxp  8076  frxp2  8094  findcard  9098  pssnn  9103  ssfi  9107  fiint  9237  marypha1lem  9346  dfom3  9568  elom3  9569  ttrclss  9641  aceq3lem  10042  dfac3  10043  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  dfacacn  10064  dfac13  10065  kmlem1  10073  kmlem10  10082  fin23lem34  10268  fin23lem35  10269  zorn2lem7  10424  zornn0g  10427  axgroth6  10751  nnunb  12433  symggen  19445  gsumval3lem2  19881  gsumzaddlem  19896  dfac14  23583  i1fd  25648  chlimi  31305  ssdifidlprm  33518  zarclssn  34017  ddemeas  34380  onvf1odlem2  35286  dfon2lem4  35966  dfon2lem5  35967  dfon2lem7  35969  ttac  43464  dfac11  43490  dfac21  43494  nregmodel  45444  setrec2fun  50167