Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eximp-surprise2 Structured version   Visualization version   GIF version

Theorem eximp-surprise2 47318
Description: Show that "there exists" with an implication is always true if there exists a situation where the antecedent is false.

Those inexperienced with formal notations of classical logic may use expressions combining "there exists" with implication. This is usually a mistake, because that combination does not mean what an inexperienced person might think it means. For example, if there is some object that does not meet the precondition 𝜑, then the expression 𝑥(𝜑𝜓) as a whole is always true, no matter what 𝜓 is (𝜓 could even be false, ). New users of formal notation who use "there exists" with an implication should consider if they meant "and" instead of "implies". See eximp-surprise 47317, which shows what implication really expands to. See also empty-surprise 47315. (Contributed by David A. Wheeler, 18-Oct-2018.)

Hypothesis
Ref Expression
eximp-surprise2.1 𝑥 ¬ 𝜑
Assertion
Ref Expression
eximp-surprise2 𝑥(𝜑𝜓)

Proof of Theorem eximp-surprise2
StepHypRef Expression
1 eximp-surprise2.1 . . 3 𝑥 ¬ 𝜑
2 orc 866 . . 3 𝜑 → (¬ 𝜑𝜓))
31, 2eximii 1840 . 2 𝑥𝜑𝜓)
4 eximp-surprise 47317 . 2 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
53, 4mpbir 230 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 846  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
This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator