Theorem spvv 1990

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

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

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 1912  ax-6 1969

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

This theorem is referenced by:  chvarvv  1991  ru0  2133  nfcr  2889  ruOLD  3741  nalset  5260  dfpo2  6262  isowe2  7306  tfisi  7811  findcard2  9101  marypha1lem  9348  elirrv  9514  setind  9668  karden  9819  kmlem4  10076  axgroth3  10754  ramcl  16969  cnsubrglem  21383  alexsubALTlem3  24005  i1fd  25650  r1omhfb  35287  setindregs  35305  r1omhfbregs  35312  dfon2lem6  35999  trer  36529  eleq2w2ALT  37289  modelaxreplem1  45328  elsetrecslem  50052