Theorem spvv 1988

Description: Specialization, using implicit substitution. Version of spv 2391 with a disjoint variable condition, which does not require ax-7 2008, ax-12 2178, ax-13 2370. (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 229	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1986	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  chvarvv  1989  ru0  2128  nfcr  2881  ruOLD  3752  nalset  5268  dfpo2  6269  isowe2  7325  tfisi  7835  findcard2  9128  marypha1lem  9384  setind  9687  karden  9848  kmlem4  10107  axgroth3  10784  ramcl  17000  cnsubrglem  21333  alexsubALTlem3  23936  i1fd  25582  dfon2lem6  35776  trer  36304  eleq2w2ALT  37035  modelaxreplem1  44968  elsetrecslem  49688