Theorem spvv 1989

Description: Specialization, using implicit substitution. Version of spv 2395 with a disjoint variable condition, which does not require ax-7 2009, ax-12 2182, ax-13 2374. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)

Hypothesis

Ref	Expression
spvv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spvv	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem spvv

Step	Hyp	Ref	Expression
1		spvv.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	biimpd 229	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1987	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539

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 1911  ax-6 1968

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  chvarvv  1990  ru0  2132  nfcr  2885  ruOLD  3736  nalset  5253  dfpo2  6248  isowe2  7290  tfisi  7795  findcard2  9081  marypha1lem  9324  elirrv  9490  setind  9644  karden  9795  kmlem4  10052  axgroth3  10729  ramcl  16943  cnsubrglem  21355  alexsubALTlem3  23965  i1fd  25610  r1omhfb  35144  setindregs  35149  r1omhfbregs  35154  dfon2lem6  35851  trer  36381  eleq2w2ALT  37112  modelaxreplem1  45096  elsetrecslem  49825