Theorem spvv 2003

Description: Specialization, using implicit substitution. Version of spv 2394 with a disjoint variable condition, which does not require ax-7 2014, ax-12 2174, ax-13 2373. (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 228	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 2002	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539

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

This theorem depends on definitions:  df-bi 206  df-ex 1786

This theorem is referenced by:  chvarvv  2005  nfcr  2893  ru  3718  nalset  5240  dfpo2  6196  isowe2  7214  tfisi  7693  findcard2  8912  findcard2OLD  9017  marypha1lem  9153  setind  9475  karden  9637  kmlem4  9893  axgroth3  10571  ramcl  16711  alexsubALTlem3  23181  i1fd  24826  dfon2lem6  33743  trer  34484  bj-ru0  35110  eleq2w2ALT  35199  elsetrecslem  46356