Theorem spvv 2020

Description: Specialization, using implicit substitution. Version of spv 2422 with a disjoint variable condition, which does not require ax-7 2040, ax-12 2212, ax-13 2401. (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 232	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 2018	1 ⊢ (∀𝑥𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  chvarvv  2021  ru0  2163  nfcr  2912  nalsetOLD  5268  dfpo2  6299  isowe2  7359  tfisi  7871  findcard2  9184  marypha1lem  9429  elirrv  9595  elirrvOLD  9596  setind  9752  kardenOLD  9964  kmlem4  10236  axgroth3  10920  ramcl  17213  cnsubrglem  21729  alexsubALTlem3  24374  i1fd  26008  r1omhfb  35791  setindregs  35855  r1omhfbregs  35862  dfon2lem6  36643  trer  37197  axtco1from2  37356  axtcond  37359  axuntco  37360  eleq2w2ALT  38055  modelaxreplem1  46062  elsetrecslem  50961