Theorem spvv 2018

Description: Specialization, using implicit substitution. Version of spv 2425 with a disjoint variable condition, which does not require ax-7 2038, ax-12 2213, ax-13 2404. (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 2016	1 ⊢ (∀𝑥𝜑 → 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997

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

This theorem is referenced by:  chvarvv  2019  ru0  2162  nfcr  2915  nalsetOLD  5279  dfpo2  6299  isowe2  7350  tfisi  7856  findcard2  9150  marypha1lem  9394  elirrv  9560  elirrvOLD  9561  setind  9717  karden  9882  kmlem4  10138  axgroth3  10817  ramcl  17090  cnsubrglem  21548  alexsubALTlem3  24187  i1fd  25821  r1omhfb  35489  setindregs  35524  r1omhfbregs  35531  dfon2lem6  36259  trer  36808  axtco1from2  36967  axtcond  36970  axuntco  36971  eleq2w2ALT  37664  modelaxreplem1  45670  elsetrecslem  50460