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 9977, and (in minimal propositional calculus), so by bd0 9944, 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 9939 | . . 3 BOUNDED |
3 | ax-bdeq 9940 | . . . . . 6 BOUNDED | |
4 | 1, 3 | ax-bdim 9934 | . . . . 5 BOUNDED |
5 | 4 | ax-bdal 9938 | . . . 4 BOUNDED |
6 | 5 | ax-bdex 9939 | . . 3 BOUNDED |
7 | 2, 6 | ax-bdan 9935 | . 2 BOUNDED |
8 | reu3 2731 | . 2 | |
9 | 7, 8 | bd0r 9945 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wral 2306 wrex 2307 wreu 2308 BOUNDED wbd 9932 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-bd0 9933 ax-bdim 9934 ax-bdan 9935 ax-bdal 9938 ax-bdex 9939 ax-bdeq 9940 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-cleq 2033 df-clel 2036 df-ral 2311 df-rex 2312 df-reu 2313 df-rmo 2314 |
This theorem is referenced by: bdrmo 9976 |
Copyright terms: Public domain | W3C validator |