Theorem spcv 3588

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   = wceq 1539   ∈ wcel 2107  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465

This theorem is referenced by:  morex  3707  al0ssb  5288  rext  5433  relop  5841  dfpo2  6296  frxp  8133  frxp2  8151  findcard  9185  pssnn  9190  ssfi  9195  fiint  9348  fiintOLD  9349  marypha1lem  9455  dfom3  9669  elom3  9670  ttrclss  9742  aceq3lem  10142  dfac3  10143  dfac5lem4  10148  dfac5lem4OLD  10150  dfac8  10158  dfac9  10159  dfacacn  10164  dfac13  10165  kmlem1  10173  kmlem10  10182  fin23lem34  10368  fin23lem35  10369  zorn2lem7  10524  zornn0g  10527  axgroth6  10850  nnunb  12505  symggen  19456  gsumval3lem2  19892  gsumzaddlem  19907  dfac14  23572  i1fd  25652  chlimi  31181  ssdifidlprm  33421  zarclssn  33831  ddemeas  34196  dfon2lem4  35746  dfon2lem5  35747  dfon2lem7  35749  ttac  43011  dfac11  43037  dfac21  43041  setrec2fun  49219