Theorem spvv 2023

Description: Specialization, using implicit substitution. Version of spv 2425 with a disjoint variable condition, which does not require ax-7 2043, ax-12 2216, ax-13 2404. (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 2021	1 ⊢ (∀𝑥𝜑 → 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002

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

This theorem is used by:  chvarvv  2024  ru0  2166  nfcr  2916  nalsetOLD  5273  dfpo2  6320  isowe2  7384  tfisi  7897  findcard2  9211  marypha1lem  9455  elirrv  9621  elirrvOLD  9622  setind  9778  kardenOLD  9990  kmlem4  10262  axgroth3  10946  ramcl  17239  cnsubrglem  21756  alexsubALTlem3  24401  i1fd  26035  eqhf  35833  setindregs  35911  eqhfregs  35918  elpssmo  36649  dfon2lem6  36741  trer  37295  axtco1from2  37454  axtcond  37457  axuntco  37458  eleq2w2ALT  38166  modelaxreplem1  46174  elsetrecslem  51082