Theorem spcv 3561

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114  Vcvv 3442

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444

This theorem is referenced by:  morex  3679  al0ssb  5255  rext  5403  relop  5807  dfpo2  6262  frxp  8078  frxp2  8096  findcard  9100  pssnn  9105  ssfi  9109  fiint  9239  marypha1lem  9348  dfom3  9568  elom3  9569  ttrclss  9641  aceq3lem  10042  dfac3  10043  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  dfacacn  10064  dfac13  10065  kmlem1  10073  kmlem10  10082  fin23lem34  10268  fin23lem35  10269  zorn2lem7  10424  zornn0g  10427  axgroth6  10751  nnunb  12409  symggen  19411  gsumval3lem2  19847  gsumzaddlem  19862  dfac14  23574  i1fd  25650  chlimi  31321  ssdifidlprm  33550  zarclssn  34050  ddemeas  34413  onvf1odlem2  35317  dfon2lem4  35997  dfon2lem5  35998  dfon2lem7  36000  ttac  43390  dfac11  43416  dfac21  43420  nregmodel  45370  setrec2fun  50048