Theorem spvv 2000

Description: Specialization, using implicit substitution. Version of spv 2392 with a disjoint variable condition, which does not require ax-7 2011, ax-12 2171, 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 228	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1999	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 1797  ax-4 1811  ax-5 1913  ax-6 1971

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

This theorem is referenced by:  chvarvv  2002  nfcr  2888  ru  3775  nalset  5312  dfpo2  6292  isowe2  7343  tfisi  7844  findcard2  9160  findcard2OLD  9280  marypha1lem  9424  setind  9725  karden  9886  kmlem4  10144  axgroth3  10822  ramcl  16958  alexsubALTlem3  23544  i1fd  25189  dfon2lem6  34748  trer  35189  bj-ru0  35811  eleq2w2ALT  35916  elsetrecslem  47697