Theorem spcv 3589

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466

This theorem is referenced by:  morex  3707  al0ssb  5283  rext  5428  relop  5835  dfpo2  6290  frxp  8130  frxp2  8148  findcard  9182  pssnn  9187  ssfi  9192  fiint  9343  fiintOLD  9344  marypha1lem  9450  dfom3  9666  elom3  9667  ttrclss  9739  aceq3lem  10139  dfac3  10140  dfac5lem4  10145  dfac5lem4OLD  10147  dfac8  10155  dfac9  10156  dfacacn  10161  dfac13  10162  kmlem1  10170  kmlem10  10179  fin23lem34  10365  fin23lem35  10366  zorn2lem7  10521  zornn0g  10524  axgroth6  10847  nnunb  12502  symggen  19456  gsumval3lem2  19892  gsumzaddlem  19907  dfac14  23561  i1fd  25639  chlimi  31220  ssdifidlprm  33478  zarclssn  33909  ddemeas  34272  dfon2lem4  35809  dfon2lem5  35810  dfon2lem7  35812  ttac  43035  dfac11  43061  dfac21  43065  nregmodel  45017  setrec2fun  49536