Theorem spvv 1988

Description: Specialization, using implicit substitution. Version of spv 2392 with a disjoint variable condition, which does not require ax-7 2008, ax-12 2178, ax-13 2371. (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 1986	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  1989  ru0  2128  nfcr  2882  ruOLD  3755  nalset  5271  dfpo2  6272  isowe2  7328  tfisi  7838  findcard2  9134  marypha1lem  9391  setind  9694  karden  9855  kmlem4  10114  axgroth3  10791  ramcl  17007  cnsubrglem  21340  alexsubALTlem3  23943  i1fd  25589  dfon2lem6  35783  trer  36311  eleq2w2ALT  37042  modelaxreplem1  44975  elsetrecslem  49692