Theorem spvv 1998

Description: Specialization, using implicit substitution. Version of spv 2391 with a disjoint variable condition, which does not require ax-7 2009, ax-12 2169, ax-13 2370. (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 228	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1997	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537

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

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

This theorem is referenced by:  chvarvv  2000  nfcr  2890  ru  3720  nalset  5246  dfpo2  6214  isowe2  7253  tfisi  7737  findcard2  8985  findcard2OLD  9100  marypha1lem  9236  setind  9536  karden  9697  kmlem4  9955  axgroth3  10633  ramcl  16775  alexsubALTlem3  23245  i1fd  24890  dfon2lem6  33809  trer  34550  bj-ru0  35175  eleq2w2ALT  35264  elsetrecslem  46462