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

Theorem spimevw 2002
Description: Existential introduction, using implicit substitution. This is to spimew 1975 what spimvw 2003 is to spimw 1974. Version of spimev 2411 and spimefv 2199 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 1912 . 2 (𝜑 → ∀𝑥𝜑)
2 spimevw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2spimew 1975 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  zfpair  5295  fvn0ssdmfun  6815  bj-dtru  34148  sn-dtru  39241  refimssco  40118  rlimdmafv  43556  rlimdmafv2  43637  elsprel  43815
  Copyright terms: Public domain W3C validator