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 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559   ∈ wcel 2141  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455

This theorem is referenced by:  morex  3680  al0ssb  5255  rext  5412  relop  5818  dfpo2  6278  frxp  8100  frxp2  8118  findcard  9126  pssnn  9131  ssfi  9135  fiint  9265  marypha1lem  9373  dfom3  9596  elom3  9597  ttrclss  9669  aceq3lem  10070  dfac3  10071  dfac5lem4  10076  dfac5lem4OLD  10078  dfac8  10086  dfac9  10087  dfacacn  10092  dfac13  10093  kmlem1  10101  kmlem10  10110  fin23lem34  10297  fin23lem35  10298  zorn2lem7  10453  zornn0g  10456  axgroth6  10780  nnunb  12471  symggen  19501  gsumval3lem2  19937  gsumzaddlem  19952  dfac14  23666  i1fd  25731  chlimi  31394  ssdifidlprm  33606  zarclssn  34131  ddemeas  34494  onvf1odlem2  35408  dfon2lem4  36095  dfon2lem5  36096  dfon2lem7  36098  ttac  43574  dfac11  43600  dfac21  43604  nregmodel  45554  setrec2fun  50274