Theorem spvv 1996

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

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

This theorem is referenced by:  chvarvv  1998  ru0  2127  nfcr  2895  ruOLD  3787  nalset  5313  dfpo2  6316  isowe2  7370  tfisi  7880  findcard2  9204  marypha1lem  9473  setind  9774  karden  9935  kmlem4  10194  axgroth3  10871  ramcl  17067  cnsubrglem  21434  alexsubALTlem3  24057  i1fd  25716  dfon2lem6  35789  trer  36317  eleq2w2ALT  37048  modelaxreplem1  44995  elsetrecslem  49218