Theorem spcv 3560

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  morex  3677  al0ssb  5262  rext  5416  relop  5828  dfpo2  6298  frxp  8136  frxp2  8154  findcard  9172  pssnn  9177  ssfi  9181  fiint  9311  marypha1lem  9418  dfom3  9641  elom3  9642  ttrclss  9714  setrec2fun  9966  aceq3lem  10192  dfac3  10193  dfac5lem4  10198  dfac8  10207  dfac9  10208  dfacacn  10213  dfac13  10214  kmlem1  10222  kmlem10  10231  fin23lem34  10417  fin23lem35  10418  zorn2lem7  10573  zornn0g  10576  axgroth6  10906  nnunb  12595  symggen  19677  gsumval3lem2  20113  gsumzaddlem  20128  ssdifidlprm  21635  dfac14  23930  i1fd  25995  chlimi  31829  zarclssn  34498  ddemeas  34862  onvf1odlem2  35866  dfon2lem4  36528  dfon2lem5  36529  dfon2lem7  36531  ttac  44022  dfac11  44048  dfac21  44052  nregmodel  45985