Theorem spvv 2007

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974

This theorem depends on definitions:  df-bi 210  df-ex 1787

This theorem is referenced by:  chvarvv  2009  nfcr  2884  ru  3678  nalset  5178  isowe2  7110  tfisi  7586  findcard2  8756  findcard2OLD  8827  marypha1lem  8963  setind  9242  karden  9390  kmlem4  9646  axgroth3  10324  ramcl  16458  alexsubALTlem3  22793  i1fd  24426  dfpo2  33286  dfon2lem6  33328  trer  34135  bj-ru0  34743  eleq2w2ALT  34832  elsetrecslem  45841