Theorem spcv 3595

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541   ∈ wcel 2106  Vcvv 3474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  morex  3715  al0ssb  5308  rext  5448  relop  5850  dfpo2  6295  frxp  8114  frxp2  8132  findcard  9165  pssnn  9170  ssfi  9175  pssnnOLD  9267  fiint  9326  marypha1lem  9430  dfom3  9644  elom3  9645  ttrclss  9717  aceq3lem  10117  dfac3  10118  dfac5lem4  10123  dfac8  10132  dfac9  10133  dfacacn  10138  dfac13  10139  kmlem1  10147  kmlem10  10156  fin23lem34  10343  fin23lem35  10344  zorn2lem7  10499  zornn0g  10502  axgroth6  10825  nnunb  12470  symggen  19340  gsumval3lem2  19776  gsumzaddlem  19791  dfac14  23129  i1fd  25205  chlimi  30525  zarclssn  32922  ddemeas  33303  dfon2lem4  34833  dfon2lem5  34834  dfon2lem7  34836  ttac  41863  dfac11  41892  dfac21  41896  setrec2fun  47821