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

Theorem spimevw 1999
Description: Existential introduction, using implicit substitution. This is to spimew 1976 what spimvw 2000 is to spimw 1975. Version of spimev 2391 and spimefv 2192 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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 spimevw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2spimew 1976 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  dtruALT2  5330  zfpair  5381  exneq  5397  dtruOLD  5403  fvn0ssdmfun  7030  onsupmaxb  41602  refimssco  41953  rlimdmafv  45483  rlimdmafv2  45564  elsprel  45741
  Copyright terms: Public domain W3C validator