Description: There is no "surprise" in a for-all with implication if there exists a value where the antecedent is true. This is one way to prevent for-all with implication from allowing anything. For a contrast, see alimp-surprise . The allsome quantifier also counters this problem, see df-alsi . (Contributed by David A. Wheeler, 27-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | alimp-no-surprise | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.82 | |
|
2 | 1 | albii | |
3 | alnex | |
|
4 | 2 3 | sylbb | |
5 | imnan | |
|
6 | 4 5 | mpbi | |
7 | 19.26 | |
|
8 | 7 | anbi2ci | |
9 | 3anass | |
|
10 | 3anrot | |
|
11 | 8 9 10 | 3bitr2i | |
12 | 6 11 | mtbi | |