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  3728  nalsetOLD  5250  dfpo2  6254  isowe2  7298  tfisi  7803  findcard2  9092  marypha1lem  9339  elirrv  9505  setind  9659  karden  9810  kmlem4  10067  axgroth3  10745  ramcl  16991  cnsubrglem  21406  alexsubALTlem3  24024  i1fd  25658  r1omhfb  35272  setindregs  35290  r1omhfbregs  35297  dfon2lem6  35984  trer  36514  axtco1from2  36673  axtcond  36676  axuntco  36677  eleq2w2ALT  37370  modelaxreplem1  45423  elsetrecslem  50186