Theorem spvv 2021

Description: Specialization, using implicit substitution. Version of spv 2423 with a disjoint variable condition, which does not require ax-7 2041, ax-12 2213, ax-13 2402. (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  2913  nalsetOLD  5269  dfpo2  6292  isowe2  7350  tfisi  7859  findcard2  9164  marypha1lem  9409  elirrv  9575  elirrvOLD  9576  setind  9732  kardenOLD  9941  kmlem4  10213  axgroth3  10897  ramcl  17187  cnsubrglem  21703  alexsubALTlem3  24348  i1fd  25982  r1omhfb  35717  setindregs  35771  r1omhfbregs  35778  dfon2lem6  36520  trer  37074  axtco1from2  37233  axtcond  37236  axuntco  37237  eleq2w2ALT  37930  modelaxreplem1  45920  elsetrecslem  50736