Theorem spvv 2011

Description: Specialization, using implicit substitution. Version of spv 2427 with a disjoint variable condition, which does not require ax-7 2031, ax-12 2215, ax-13 2406. (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 232	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 2009	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  chvarvv  2012  ru0  2164  nfcr  2917  nalsetOLD  5269  dfpo2  6286  isowe2  7338  tfisi  7843  findcard2  9137  marypha1lem  9381  elirrv  9547  elirrvOLD  9548  setind  9704  karden  9869  kmlem4  10125  axgroth3  10804  ramcl  17077  cnsubrglem  21524  alexsubALTlem3  24163  i1fd  25797  r1omhfb  35415  setindregs  35433  r1omhfbregs  35440  dfon2lem6  36144  trer  36684  axtco1from2  36843  axtcond  36846  axuntco  36847  eleq2w2ALT  37539  modelaxreplem1  45546  elsetrecslem  50329