Theorem spcv 3605

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2106  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480

This theorem is referenced by:  morex  3728  al0ssb  5314  rext  5459  relop  5864  dfpo2  6318  frxp  8150  frxp2  8168  findcard  9202  pssnn  9207  ssfi  9212  fiint  9364  fiintOLD  9365  marypha1lem  9471  dfom3  9685  elom3  9686  ttrclss  9758  aceq3lem  10158  dfac3  10159  dfac5lem4  10164  dfac5lem4OLD  10166  dfac8  10174  dfac9  10175  dfacacn  10180  dfac13  10181  kmlem1  10189  kmlem10  10198  fin23lem34  10384  fin23lem35  10385  zorn2lem7  10540  zornn0g  10543  axgroth6  10866  nnunb  12520  symggen  19503  gsumval3lem2  19939  gsumzaddlem  19954  dfac14  23642  i1fd  25730  chlimi  31263  ssdifidlprm  33466  zarclssn  33834  ddemeas  34217  dfon2lem4  35768  dfon2lem5  35769  dfon2lem7  35771  ttac  43025  dfac11  43051  dfac21  43055  setrec2fun  48923