MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spimevw Structured version   Visualization version   GIF version

Theorem spimevw 1994
Description: Existential introduction, using implicit substitution. This is to spimew 1971 what spimvw 1995 is to spimw 1970. Version of spimev 2397 and spimefv 2198 with an additional disjoint variable condition, using only Tarski's FOL axiom schemes. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 17-Mar-2020.)
Hypothesis
Ref Expression
spimevw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
spimevw (𝜑 → ∃𝑥𝜓)
Distinct variable groups:   𝑥,𝑦   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem spimevw
StepHypRef Expression
1 ax-5 1910 . 2 (𝜑 → ∀𝑥𝜑)
2 spimevw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2spimew 1971 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  dtruALT2  5370  zfpair  5421  axprlem3  5425  exneq  5440  dtruOLD  5446  fvn0ssdmfun  7094  onsupmaxb  43251  refimssco  43620  rlimdmafv  47189  rlimdmafv2  47270  elsprel  47462
  Copyright terms: Public domain W3C validator