Theorem spcv 3566

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  morex  3684  al0ssb  5273  rext  5431  relop  5838  dfpo2  6301  frxp  8124  frxp2  8142  findcard  9151  pssnn  9156  ssfi  9160  fiint  9289  marypha1lem  9396  dfom3  9619  elom3  9620  ttrclss  9692  aceq3lem  10116  dfac3  10117  dfac5lem4  10122  dfac8  10131  dfac9  10132  dfacacn  10137  dfac13  10138  kmlem1  10146  kmlem10  10155  fin23lem34  10341  fin23lem35  10342  zorn2lem7  10497  zornn0g  10500  axgroth6  10824  nnunb  12511  symggen  19564  gsumval3lem2  20000  gsumzaddlem  20015  ssdifidlprm  21516  dfac14  23806  i1fd  25871  chlimi  31633  zarclssn  34303  ddemeas  34667  onvf1odlem2  35621  dfon2lem4  36289  dfon2lem5  36290  dfon2lem7  36292  ttac  43796  dfac11  43822  dfac21  43826  nregmodel  45759  setrec2fun  50503