Theorem eximp-surprise2

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 ph , then the expression E. x ( ph -> ps ) as a whole is always true, no matter what ps is ( ps could even be false, F. ). New users of formal notation who use "there exists" with an implication should consider if they meant "and" instead of "implies". See eximp-surprise , which shows what implication really expands to. See also empty-surprise . (Contributed by David A. Wheeler, 18-Oct-2018)

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

Proof

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