Theorem spcv 3573

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   = wceq 1567   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  morex  3691  al0ssb  5270  rext  5427  relop  5834  dfpo2  6294  frxp  8118  frxp2  8136  findcard  9144  pssnn  9149  ssfi  9153  fiint  9282  marypha1lem  9389  dfom3  9612  elom3  9613  ttrclss  9685  aceq3lem  10100  dfac3  10101  dfac5lem4  10106  dfac8  10115  dfac9  10116  dfacacn  10121  dfac13  10122  kmlem1  10130  kmlem10  10139  fin23lem34  10326  fin23lem35  10327  zorn2lem7  10482  zornn0g  10485  axgroth6  10809  nnunb  12496  symggen  19536  gsumval3lem2  19972  gsumzaddlem  19987  ssdifidlprm  21451  dfac14  23740  i1fd  25805  chlimi  31523  zarclssn  34204  ddemeas  34567  onvf1odlem2  35483  dfon2lem4  36171  dfon2lem5  36172  dfon2lem7  36174  ttac  43648  dfac11  43674  dfac21  43678  nregmodel  45611  setrec2fun  50348