Theorem spcv 3500

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599   = wceq 1601   ∈ wcel 2106  Vcvv 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399

This theorem is referenced by:  morex  3601  al0ssb  5027  rext  5148  relop  5518  frxp  7568  pssnn  8466  findcard  8487  fiint  8525  marypha1lem  8627  dfom3  8841  elom3  8842  aceq3lem  9276  dfac3  9277  dfac5lem4  9282  dfac8  9292  dfac9  9293  dfacacn  9298  dfac13  9299  kmlem1  9307  kmlem10  9316  fin23lem34  9503  fin23lem35  9504  zorn2lem7  9659  zornn0g  9662  axgroth6  9985  nnunb  11638  symggen  18273  gsumval3lem2  18693  gsumzaddlem  18707  dfac14  21830  i1fd  23885  chlimi  28663  ddemeas  30897  dfpo2  32239  dfon2lem4  32279  dfon2lem5  32280  dfon2lem7  32282  ttac  38544  dfac11  38573  dfac21  38577  setrec2fun  43526