Theorem spvv 2021

Description: Specialization, using implicit substitution. Version of spv 2424 with a disjoint variable condition, which does not require ax-7 2041, ax-12 2215, ax-13 2403. (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 2019	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 1943  ax-6 2000

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

This theorem is used by:  chvarvv  2022  ru0  2164  nfcr  2914  nalsetOLD  5276  dfpo2  6298  isowe2  7355  tfisi  7859  findcard2  9163  marypha1lem  9407  elirrv  9573  elirrvOLD  9574  setind  9730  kardenOLD  9903  kmlem4  10160  axgroth3  10844  ramcl  17127  cnsubrglem  21636  alexsubALTlem3  24281  i1fd  25915  r1omhfb  35630  setindregs  35664  r1omhfbregs  35671  dfon2lem6  36373  trer  36943  axtco1from2  37102  axtcond  37105  axuntco  37106  eleq2w2ALT  37799  modelaxreplem1  45809  elsetrecslem  50633