Theorem spvv 2007

Description: Specialization, using implicit substitution. Version of spv 2423 with a disjoint variable condition, which does not require ax-7 2027, ax-12 2211, 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 231	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 2005	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  chvarvv  2008  ru0  2160  nfcr  2913  ruOLD  3743  nalsetOLD  5264  dfpo2  6279  isowe2  7330  tfisi  7835  findcard2  9129  marypha1lem  9376  elirrv  9542  elirrvOLD  9543  setind  9699  karden  9850  kmlem4  10107  axgroth3  10786  ramcl  17048  cnsubrglem  21449  alexsubALTlem3  24089  i1fd  25723  r1omhfb  35372  setindregs  35390  r1omhfbregs  35397  dfon2lem6  36100  trer  36640  axtco1from2  36799  axtcond  36802  axuntco  36803  eleq2w2ALT  37496  modelaxreplem1  45518  elsetrecslem  50284