Theorem empty-surprise2 42529

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 42528. Here we prove an extreme example: we "prove" that false is true. Of course, we actually do no such thing (see notfal 1519); 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 42535. (Contributed by David A. Wheeler, 20-Oct-2018.)

Hypothesis

Ref	Expression
empty-surprise2.1	|- -. E. x x e. A

Assertion

Ref	Expression
empty-surprise2	|- A. x e. A F.

Proof of Theorem empty-surprise2

Step	Hyp	Ref	Expression
1		empty-surprise2.1	. 2 |- -. E. x x e. A
2	1	empty-surprise 42528	1 |- A. x e. A F.

Syntax hints:   -. wn 3   F. wfal 1488   E.wex 1704   e. wcel 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-ral 2917

This theorem is referenced by: (None)