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 13044, and (in minimal propositional calculus), so by bd0 13011, 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 13006 | . . 3 BOUNDED |
3 | ax-bdeq 13007 | . . . . . 6 BOUNDED | |
4 | 1, 3 | ax-bdim 13001 | . . . . 5 BOUNDED |
5 | 4 | ax-bdal 13005 | . . . 4 BOUNDED |
6 | 5 | ax-bdex 13006 | . . 3 BOUNDED |
7 | 2, 6 | ax-bdan 13002 | . 2 BOUNDED |
8 | reu3 2869 | . 2 | |
9 | 7, 8 | bd0r 13012 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wral 2414 wrex 2415 wreu 2416 BOUNDED wbd 12999 |
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 2119 ax-bd0 13000 ax-bdim 13001 ax-bdan 13002 ax-bdal 13005 ax-bdex 13006 ax-bdeq 13007 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-cleq 2130 df-clel 2133 df-ral 2419 df-rex 2420 df-reu 2421 df-rmo 2422 |
This theorem is referenced by: bdrmo 13043 |
Copyright terms: Public domain | W3C validator |