Theorem spvv 1989

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

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

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 1968

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

This theorem is referenced by:  chvarvv  1990  ru0  2130  nfcr  2884  ruOLD  3740  nalset  5251  dfpo2  6243  isowe2  7284  tfisi  7789  findcard2  9074  marypha1lem  9317  elirrv  9483  setind  9637  karden  9788  kmlem4  10045  axgroth3  10722  ramcl  16941  cnsubrglem  21354  alexsubALTlem3  23965  i1fd  25610  r1omhfb  35121  setindregs  35126  r1omhfbregs  35131  dfon2lem6  35828  trer  36356  eleq2w2ALT  37087  modelaxreplem1  45017  elsetrecslem  49737