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  3714  al0ssb  5307  rext  5447  relop  5848  dfpo2  6292  frxp  8108  frxp2  8126  findcard  9159  pssnn  9164  ssfi  9169  pssnnOLD  9261  fiint  9320  marypha1lem  9424  dfom3  9638  elom3  9639  ttrclss  9711  aceq3lem  10111  dfac3  10112  dfac5lem4  10117  dfac8  10126  dfac9  10127  dfacacn  10132  dfac13  10133  kmlem1  10141  kmlem10  10150  fin23lem34  10337  fin23lem35  10338  zorn2lem7  10493  zornn0g  10496  axgroth6  10819  nnunb  12464  symggen  19332  gsumval3lem2  19768  gsumzaddlem  19783  dfac14  23113  i1fd  25189  chlimi  30474  zarclssn  32841  ddemeas  33222  dfon2lem4  34746  dfon2lem5  34747  dfon2lem7  34749  ttac  41760  dfac11  41789  dfac21  41793  setrec2fun  47690