Theorem spcv 3559

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

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

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  morex  3677  al0ssb  5253  rext  5396  relop  5799  dfpo2  6254  frxp  8068  frxp2  8086  findcard  9088  pssnn  9093  ssfi  9097  fiint  9227  marypha1lem  9336  dfom3  9556  elom3  9557  ttrclss  9629  aceq3lem  10030  dfac3  10031  dfac5lem4  10036  dfac5lem4OLD  10038  dfac8  10046  dfac9  10047  dfacacn  10052  dfac13  10053  kmlem1  10061  kmlem10  10070  fin23lem34  10256  fin23lem35  10257  zorn2lem7  10412  zornn0g  10415  axgroth6  10739  nnunb  12397  symggen  19399  gsumval3lem2  19835  gsumzaddlem  19850  dfac14  23562  i1fd  25638  chlimi  31309  ssdifidlprm  33539  zarclssn  34030  ddemeas  34393  onvf1odlem2  35298  dfon2lem4  35978  dfon2lem5  35979  dfon2lem7  35981  ttac  43278  dfac11  43304  dfac21  43308  nregmodel  45258  setrec2fun  49937