Theorem spcv 3565

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  morex  3683  al0ssb  5272  rext  5431  relop  5838  dfpo2  6299  frxp  8123  frxp2  8141  findcard  9149  pssnn  9154  ssfi  9158  fiint  9287  marypha1lem  9394  dfom3  9617  elom3  9618  ttrclss  9690  aceq3lem  10105  dfac3  10106  dfac5lem4  10111  dfac8  10120  dfac9  10121  dfacacn  10126  dfac13  10127  kmlem1  10135  kmlem10  10144  fin23lem34  10331  fin23lem35  10332  zorn2lem7  10487  zornn0g  10490  axgroth6  10814  nnunb  12501  symggen  19541  gsumval3lem2  19977  gsumzaddlem  19992  ssdifidlprm  21467  dfac14  23756  i1fd  25821  chlimi  31567  zarclssn  34244  ddemeas  34607  onvf1odlem2  35569  dfon2lem4  36257  dfon2lem5  36258  dfon2lem7  36260  ttac  43746  dfac11  43772  dfac21  43776  nregmodel  45709  setrec2fun  50453