Theorem spcv 3596

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  morex  3716  al0ssb  5309  rext  5449  relop  5851  dfpo2  6296  frxp  8112  frxp2  8130  findcard  9163  pssnn  9168  ssfi  9173  pssnnOLD  9265  fiint  9324  marypha1lem  9428  dfom3  9642  elom3  9643  ttrclss  9715  aceq3lem  10115  dfac3  10116  dfac5lem4  10121  dfac8  10130  dfac9  10131  dfacacn  10136  dfac13  10137  kmlem1  10145  kmlem10  10154  fin23lem34  10341  fin23lem35  10342  zorn2lem7  10497  zornn0g  10500  axgroth6  10823  nnunb  12468  symggen  19338  gsumval3lem2  19774  gsumzaddlem  19789  dfac14  23122  i1fd  25198  chlimi  30487  zarclssn  32853  ddemeas  33234  dfon2lem4  34758  dfon2lem5  34759  dfon2lem7  34761  ttac  41775  dfac11  41804  dfac21  41808  setrec2fun  47737