Theorem spvv 2003

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970

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

This theorem is referenced by:  chvarvv  2005  ru  3771  nalset  5217  isowe2  7103  tfisi  7573  findcard2  8758  marypha1lem  8897  setind  9176  karden  9324  kmlem4  9579  axgroth3  10253  ramcl  16365  alexsubALTlem3  22657  i1fd  24282  dfpo2  32991  dfon2lem6  33033  trer  33664  bj-ru0  34256  elsetrecslem  44850