Theorem spcv 3559

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  morex  3677  al0ssb  5265  rext  5423  relop  5830  dfpo2  6294  frxp  8124  frxp2  8142  findcard  9158  pssnn  9163  ssfi  9167  fiint  9296  marypha1lem  9403  dfom3  9626  elom3  9627  ttrclss  9699  aceq3lem  10123  dfac3  10124  dfac5lem4  10129  dfac8  10138  dfac9  10139  dfacacn  10144  dfac13  10145  kmlem1  10153  kmlem10  10162  fin23lem34  10348  fin23lem35  10349  zorn2lem7  10504  zornn0g  10507  axgroth6  10837  nnunb  12524  symggen  19597  gsumval3lem2  20033  gsumzaddlem  20048  ssdifidlprm  21549  dfac14  23844  i1fd  25909  chlimi  31715  zarclssn  34383  ddemeas  34747  onvf1odlem2  35701  dfon2lem4  36363  dfon2lem5  36364  dfon2lem7  36366  ttac  43877  dfac11  43903  dfac21  43907  nregmodel  45840  setrec2fun  50618