Theorem spcv 3556

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2113  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  morex  3674  al0ssb  5250  rext  5393  relop  5796  dfpo2  6251  frxp  8065  frxp2  8083  findcard  9084  pssnn  9089  ssfi  9093  fiint  9222  marypha1lem  9328  dfom3  9548  elom3  9549  ttrclss  9621  aceq3lem  10022  dfac3  10023  dfac5lem4  10028  dfac5lem4OLD  10030  dfac8  10038  dfac9  10039  dfacacn  10044  dfac13  10045  kmlem1  10053  kmlem10  10062  fin23lem34  10248  fin23lem35  10249  zorn2lem7  10404  zornn0g  10407  axgroth6  10730  nnunb  12388  symggen  19390  gsumval3lem2  19826  gsumzaddlem  19841  dfac14  23553  i1fd  25629  chlimi  31235  ssdifidlprm  33467  zarclssn  33958  ddemeas  34321  onvf1odlem2  35220  dfon2lem4  35900  dfon2lem5  35901  dfon2lem7  35903  ttac  43193  dfac11  43219  dfac21  43223  nregmodel  45174  setrec2fun  49853