Theorem spcv 3554

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  morex  3658  al0ssb  5176  rext  5306  relop  5685  frxp  7803  pssnn  8720  findcard  8741  fiint  8779  marypha1lem  8881  dfom3  9094  elom3  9095  aceq3lem  9531  dfac3  9532  dfac5lem4  9537  dfac8  9546  dfac9  9547  dfacacn  9552  dfac13  9553  kmlem1  9561  kmlem10  9570  fin23lem34  9757  fin23lem35  9758  zorn2lem7  9913  zornn0g  9916  axgroth6  10239  nnunb  11881  symggen  18590  gsumval3lem2  19019  gsumzaddlem  19034  dfac14  22223  i1fd  24285  chlimi  29017  zarclssn  31226  ddemeas  31605  dfpo2  33104  dfon2lem4  33144  dfon2lem5  33145  dfon2lem7  33147  ttac  39977  dfac11  40006  dfac21  40010  setrec2fun  45222