![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > xrex | Unicode version |
Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
xrex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xr 9080 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | reex 9037 |
. . 3
![]() ![]() ![]() ![]() | |
3 | prex 4366 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | unex 4666 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2474 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: ixxval 10880 ixxf 10882 ixxex 10883 limsuple 12227 limsuplt 12228 limsupbnd1 12231 prdsds 13641 letsr 14627 xrsbas 16672 xrsadd 16673 xrsmul 16674 xrsle 16676 xrs1mnd 16691 xrs10 16692 xrs1cmn 16693 xrge0subm 16694 xrge0cmn 16695 xrsds 16696 znle 16772 leordtval2 17230 lecldbas 17237 ispsmet 18288 isxmet 18307 imasdsf1olem 18356 blfvalps 18366 nmoffn 18698 nmofval 18701 xrsxmet 18793 xrge0gsumle 18817 xrge0tsms 18818 xrlimcnp 20760 xrge00 24161 xrge0tsmsd 24176 xrhval 24337 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-rex 2672 df-v 2918 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-sn 3780 df-pr 3781 df-uni 3976 df-xr 9080 |
Copyright terms: Public domain | W3C validator |