Theorem spvv 2021

Description: Specialization, using implicit substitution. Version of spv 2428 with a disjoint variable condition, which does not require ax-7 2041, ax-12 2216, ax-13 2407. (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  2165  nfcr  2918  nalsetOLD  5283  dfpo2  6304  isowe2  7359  tfisi  7864  findcard2  9159  marypha1lem  9403  elirrv  9569  elirrvOLD  9570  setind  9726  kardenOLD  9899  kmlem4  10156  axgroth3  10834  ramcl  17114  cnsubrglem  21604  alexsubALTlem3  24243  i1fd  25877  r1omhfb  35533  setindregs  35567  r1omhfbregs  35574  dfon2lem6  36299  trer  36868  axtco1from2  37027  axtcond  37030  axuntco  37031  eleq2w2ALT  37724  modelaxreplem1  45728  elsetrecslem  50518