Theorem empty-surprise2 48139

Description: "Prove" that false is true when using a restricted "for all" over the empty set, to demonstrate that the expression is always true if the value ranges over the empty set.

Those inexperienced with formal notations of classical logic can be surprised with what restricted "for all" does over an empty set. We proved the general case in empty-surprise 48138. Here we prove an extreme example: we "prove" that false is true. Of course, we actually do no such thing (see notfal 1562); the problem is that restricted "for all" works in ways that might seem counterintuitive to the inexperienced when given an empty set. Solutions to this can include requiring that the set not be empty or by using the allsome quantifier df-alsc 48145. (Contributed by David A. Wheeler, 20-Oct-2018.)

Hypothesis

Ref	Expression
empty-surprise2.1	⊢ ¬ ∃𝑥 𝑥 ∈ 𝐴

Assertion

Ref	Expression
empty-surprise2	⊢ ∀𝑥 ∈ 𝐴 ⊥

Proof of Theorem empty-surprise2

Step	Hyp	Ref	Expression
1		empty-surprise2.1	. 2 ⊢ ¬ ∃𝑥 𝑥 ∈ 𝐴
2	1	empty-surprise 48138	1 ⊢ ∀𝑥 ∈ 𝐴 ⊥

Syntax hints:  ¬ wn 3  ⊥wfal 1546  ∃wex 1774   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-ral 3057

This theorem is referenced by: (None)