Theorem spvv 2002

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

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

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 1969

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

This theorem is referenced by:  chvarvv  2004  ru  3767  nalset  5210  isowe2  7096  tfisi  7566  findcard2  8751  marypha1lem  8890  setind  9169  karden  9317  kmlem4  9572  axgroth3  10246  ramcl  16360  alexsubALTlem3  22652  i1fd  24277  dfpo2  33012  dfon2lem6  33054  trer  33685  bj-ru0  34277  elsetrecslem  44875