Theorem spcv 3595

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1538   = wceq 1540   ∈ wcel 2105  Vcvv 3473

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475

This theorem is referenced by:  morex  3715  al0ssb  5308  rext  5448  relop  5850  dfpo2  6295  frxp  8117  frxp2  8135  findcard  9169  pssnn  9174  ssfi  9179  pssnnOLD  9271  fiint  9330  marypha1lem  9434  dfom3  9648  elom3  9649  ttrclss  9721  aceq3lem  10121  dfac3  10122  dfac5lem4  10127  dfac8  10136  dfac9  10137  dfacacn  10142  dfac13  10143  kmlem1  10151  kmlem10  10160  fin23lem34  10347  fin23lem35  10348  zorn2lem7  10503  zornn0g  10506  axgroth6  10829  nnunb  12475  symggen  19386  gsumval3lem2  19822  gsumzaddlem  19837  dfac14  23442  i1fd  25530  chlimi  30920  zarclssn  33317  ddemeas  33698  dfon2lem4  35228  dfon2lem5  35229  dfon2lem7  35231  ttac  42238  dfac11  42267  dfac21  42271  setrec2fun  47899