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  3740  nalset  5259  dfpo2  6255  isowe2  7298  tfisi  7803  findcard2  9093  marypha1lem  9340  elirrv  9506  setind  9660  karden  9811  kmlem4  10068  axgroth3  10746  ramcl  16961  cnsubrglem  21375  alexsubALTlem3  23997  i1fd  25642  r1omhfb  35249  setindregs  35267  r1omhfbregs  35274  dfon2lem6  35961  trer  36491  eleq2w2ALT  37223  modelaxreplem1  45255  elsetrecslem  49980