Theorem spvv 1996

Description: Specialization, using implicit substitution. Version of spv 2401 with a disjoint variable condition, which does not require ax-7 2007, ax-12 2178, ax-13 2380. (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 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967

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

This theorem is referenced by:  chvarvv  1998  ru0  2127  nfcr  2898  ruOLD  3803  nalset  5331  dfpo2  6327  isowe2  7386  tfisi  7896  findcard2  9230  marypha1lem  9502  setind  9803  karden  9964  kmlem4  10223  axgroth3  10900  ramcl  17076  cnsubrglem  21457  alexsubALTlem3  24078  i1fd  25735  dfon2lem6  35752  trer  36282  eleq2w2ALT  37013  elsetrecslem  48791