Theorem spvv 1996

Description: Specialization, using implicit substitution. Version of spv 2397 with a disjoint variable condition, which does not require ax-7 2007, ax-12 2177, ax-13 2376. (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 1995	1 ⊢ (∀𝑥𝜑 → 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

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

This theorem is referenced by:  chvarvv  1998  ru0  2127  nfcr  2888  ruOLD  3764  nalset  5283  dfpo2  6285  isowe2  7343  tfisi  7854  findcard2  9178  marypha1lem  9445  setind  9748  karden  9909  kmlem4  10168  axgroth3  10845  ramcl  17049  cnsubrglem  21384  alexsubALTlem3  23987  i1fd  25634  dfon2lem6  35806  trer  36334  eleq2w2ALT  37065  modelaxreplem1  45003  elsetrecslem  49563