Theorem spvv 1993

Description: Specialization, using implicit substitution. Version of spv 2395 with a disjoint variable condition, which does not require ax-7 2004, ax-12 2174, 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 1992	1 ⊢ (∀𝑥𝜑 → 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964

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

This theorem is referenced by:  chvarvv  1995  ru0  2124  nfcr  2892  ruOLD  3789  nalset  5318  dfpo2  6317  isowe2  7369  tfisi  7879  findcard2  9202  marypha1lem  9470  setind  9771  karden  9932  kmlem4  10191  axgroth3  10868  ramcl  17062  cnsubrglem  21451  alexsubALTlem3  24072  i1fd  25729  dfon2lem6  35769  trer  36298  eleq2w2ALT  37029  modelaxreplem1  44942  elsetrecslem  48929