Theorem spvv 1995

Description: Specialization, using implicit substitution. Version of spv 2401 with a disjoint variable condition, which does not require ax-7 2015, ax-12 2189, ax-13 2380. (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 230	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1993	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  chvarvv  1996  ru0  2138  nfcr  2892  ruOLD  3729  nalsetOLD  5244  dfpo2  6254  isowe2  7301  tfisi  7806  findcard2  9096  marypha1lem  9343  elirrv  9509  elirrvOLD  9510  setind  9666  karden  9817  kmlem4  10074  axgroth3  10752  ramcl  16998  cnsubrglem  21399  alexsubALTlem3  24039  i1fd  25673  r1omhfb  35300  setindregs  35318  r1omhfbregs  35325  dfon2lem6  36021  trer  36551  axtco1from2  36710  axtcond  36713  axuntco  36714  eleq2w2ALT  37407  modelaxreplem1  45429  elsetrecslem  50196