Theorem eximp-surprise2 42531

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 42530, which shows what implication really expands to. See also empty-surprise 42528. (Contributed by David A. Wheeler, 18-Oct-2018.)

Hypothesis

Ref	Expression
eximp-surprise2.1	⊢ ∃𝑥 ¬ 𝜑

Assertion

Ref	Expression
eximp-surprise2	⊢ ∃𝑥(𝜑 → 𝜓)

Proof of Theorem eximp-surprise2

Step	Hyp	Ref	Expression
1		eximp-surprise2.1	. . 3 ⊢ ∃𝑥 ¬ 𝜑
2		orc 400	. . 3 ⊢ (¬ 𝜑 → (¬ 𝜑 ∨ 𝜓))
3	1, 2	eximii 1764	. 2 ⊢ ∃𝑥(¬ 𝜑 ∨ 𝜓)
4		eximp-surprise 42530	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ ∃𝑥(¬ 𝜑 ∨ 𝜓))
5	3, 4	mpbir 221	1 ⊢ ∃𝑥(𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705

This theorem is referenced by: (None)