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 1567   = wceq 1569   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  morex  3676  al0ssb  5261  rext  5415  relop  5827  dfpo2  6299  frxp  8141  frxp2  8164  findcard  9183  pssnn  9188  ssfi  9192  fiint  9322  marypha1lem  9429  dfom3  9652  elom3  9653  ttrclss  9725  setrec2fun  9977  aceq3lem  10203  dfac3  10204  dfac5lem4  10209  dfac8  10218  dfac9  10219  dfacacn  10224  dfac13  10225  kmlem1  10233  kmlem10  10242  fin23lem34  10428  fin23lem35  10429  zorn2lem7  10584  zornn0g  10587  axgroth6  10917  nnunb  12606  symggen  19690  gsumval3lem2  20126  gsumzaddlem  20141  ssdifidlprm  21648  dfac14  23943  i1fd  26008  chlimi  31842  zarclssn  34552  ddemeas  34916  dfac16  35811  acwer1prclem  35816  onvf1odlem2  35952  dfon2lem4  36641  dfon2lem5  36642  dfon2lem7  36644  ttac  44137  dfac11  44158  dfac21  44162  nregmodel  46101