Theorem spcv 3534

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  morex  3649  al0ssb  5227  rext  5358  relop  5748  dfpo2  6188  frxp  7938  findcard  8908  pssnn  8913  ssfi  8918  pssnnOLD  8969  fiint  9021  marypha1lem  9122  dfom3  9335  elom3  9336  aceq3lem  9807  dfac3  9808  dfac5lem4  9813  dfac8  9822  dfac9  9823  dfacacn  9828  dfac13  9829  kmlem1  9837  kmlem10  9846  fin23lem34  10033  fin23lem35  10034  zorn2lem7  10189  zornn0g  10192  axgroth6  10515  nnunb  12159  symggen  18993  gsumval3lem2  19422  gsumzaddlem  19437  dfac14  22677  i1fd  24750  chlimi  29497  zarclssn  31725  ddemeas  32104  dfon2lem4  33668  dfon2lem5  33669  dfon2lem7  33671  ttrclss  33706  frxp2  33718  frxp3  33724  ttac  40774  dfac11  40803  dfac21  40807  setrec2fun  46284