Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdreu | Unicode version |
Description: Boundedness of
existential uniqueness.
Remark regarding restricted quantifiers: the formula need not be bounded even if and are. Indeed, is bounded by bdcvv 13055, and (in minimal propositional calculus), so by bd0 13022, if were bounded when is bounded, then would be bounded as well when is bounded, which is not the case. The same remark holds with . (Contributed by BJ, 16-Oct-2019.) |
Ref | Expression |
---|---|
bdreu.1 | BOUNDED |
Ref | Expression |
---|---|
bdreu | BOUNDED |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdreu.1 | . . . 4 BOUNDED | |
2 | 1 | ax-bdex 13017 | . . 3 BOUNDED |
3 | ax-bdeq 13018 | . . . . . 6 BOUNDED | |
4 | 1, 3 | ax-bdim 13012 | . . . . 5 BOUNDED |
5 | 4 | ax-bdal 13016 | . . . 4 BOUNDED |
6 | 5 | ax-bdex 13017 | . . 3 BOUNDED |
7 | 2, 6 | ax-bdan 13013 | . 2 BOUNDED |
8 | reu3 2874 | . 2 | |
9 | 7, 8 | bd0r 13023 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wral 2416 wrex 2417 wreu 2418 BOUNDED wbd 13010 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-bd0 13011 ax-bdim 13012 ax-bdan 13013 ax-bdal 13016 ax-bdex 13017 ax-bdeq 13018 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-cleq 2132 df-clel 2135 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 |
This theorem is referenced by: bdrmo 13054 |
Copyright terms: Public domain | W3C validator |