Theorem spvv 1989

Description: Specialization, using implicit substitution. Version of spv 2397 with a disjoint variable condition, which does not require ax-7 2009, ax-12 2184, ax-13 2376. (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  2132  nfcr  2888  ruOLD  3739  nalset  5258  dfpo2  6254  isowe2  7296  tfisi  7801  findcard2  9089  marypha1lem  9336  elirrv  9502  setind  9656  karden  9807  kmlem4  10064  axgroth3  10742  ramcl  16957  cnsubrglem  21371  alexsubALTlem3  23993  i1fd  25638  r1omhfb  35268  setindregs  35286  r1omhfbregs  35293  dfon2lem6  35980  trer  36510  eleq2w2ALT  37248  modelaxreplem1  45215  elsetrecslem  49940