Theorem spcv 3563

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  morex  3680  al0ssb  5268  rext  5423  relop  5838  dfpo2  6325  frxp  8175  frxp2  8198  findcard  9217  pssnn  9222  ssfi  9226  fiint  9356  marypha1lem  9462  dfom3  9685  elom3  9686  ttrclss  9758  setrec2fun  10010  aceq3lem  10238  dfac3  10239  dfac5lem4  10244  dfac8  10253  dfac9  10254  dfacacn  10259  dfac13  10260  kmlem1  10268  kmlem10  10277  fin23lem34  10463  fin23lem35  10464  zorn2lem7  10619  zornn0g  10622  axgroth6  10952  nnunb  12642  symggen  19735  gsumval3lem2  20171  gsumzaddlem  20186  ssdifidlprm  21693  dfac14  23992  i1fd  26057  chlimi  31893  zarclssn  34616  ddemeas  34980  dfac16  35887  acwer1prclem  35892  onvf1odlem2  36073  elpssmo  36673  dfon2lem4  36763  dfon2lem5  36764  dfon2lem7  36766  ttac  44309  dfac11  44330  dfac21  44334  nregmodel  46271