Theorem spvv 1988

Description: Specialization, using implicit substitution. Version of spv 2391 with a disjoint variable condition, which does not require ax-7 2008, ax-12 2178, 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 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  2881  ruOLD  3743  nalset  5255  dfpo2  6248  isowe2  7291  tfisi  7799  findcard2  9088  marypha1lem  9342  elirrv  9508  setind  9649  karden  9810  kmlem4  10067  axgroth3  10744  ramcl  16959  cnsubrglem  21341  alexsubALTlem3  23952  i1fd  25598  setindregs  35067  dfon2lem6  35764  trer  36292  eleq2w2ALT  37023  modelaxreplem1  44955  elsetrecslem  49688