Theorem spcv 3543

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  morex  3660  al0ssb  5230  rext  5387  relop  5792  dfpo2  6247  frxp  8066  frxp2  8084  findcard  9088  pssnn  9093  ssfi  9097  fiint  9227  marypha1lem  9336  dfom3  9559  elom3  9560  ttrclss  9632  aceq3lem  10033  dfac3  10034  dfac5lem4  10039  dfac5lem4OLD  10041  dfac8  10049  dfac9  10050  dfacacn  10055  dfac13  10056  kmlem1  10064  kmlem10  10073  fin23lem34  10259  fin23lem35  10260  zorn2lem7  10415  zornn0g  10418  axgroth6  10742  nnunb  12424  symggen  19436  gsumval3lem2  19872  gsumzaddlem  19887  dfac14  23601  i1fd  25666  chlimi  31323  ssdifidlprm  33541  zarclssn  34057  ddemeas  34420  onvf1odlem2  35332  dfon2lem4  36012  dfon2lem5  36013  dfon2lem7  36015  ttac  43481  dfac11  43507  dfac21  43511  nregmodel  45461  setrec2fun  50182