![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elxr | Unicode version |
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
elxr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xr 8010 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq2i 2254 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | elun 3288 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | pnfex 8025 |
. . . . 5
![]() ![]() ![]() ![]() | |
5 | mnfxr 8028 |
. . . . . 6
![]() ![]() ![]() ![]() | |
6 | 5 | elexi 2761 |
. . . . 5
![]() ![]() ![]() ![]() |
7 | 4, 6 | elpr2 3626 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | orbi2i 763 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3orass 982 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 8, 9 | bitr4i 187 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 2, 3, 10 | 3bitri 206 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-un 4445 ax-cnex 7916 |
This theorem depends on definitions: df-bi 117 df-3or 980 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-rex 2471 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-uni 3822 df-pnf 8008 df-mnf 8009 df-xr 8010 |
This theorem is referenced by: xrnemnf 9791 xrnepnf 9792 xrltnr 9793 xrltnsym 9807 xrlttr 9809 xrltso 9810 xrlttri3 9811 nltpnft 9828 npnflt 9829 ngtmnft 9831 nmnfgt 9832 xrrebnd 9833 xnegcl 9846 xnegneg 9847 xltnegi 9849 xrpnfdc 9856 xrmnfdc 9857 xnegid 9873 xaddcom 9875 xaddid1 9876 xnegdi 9882 xleadd1a 9887 xltadd1 9890 xlt2add 9894 xsubge0 9895 xposdif 9896 xleaddadd 9901 qbtwnxr 10272 xrmaxiflemcl 11267 xrmaxifle 11268 xrmaxiflemab 11269 xrmaxiflemlub 11270 xrmaxltsup 11280 xrmaxadd 11283 xrbdtri 11298 isxmet2d 14201 blssioo 14398 |
Copyright terms: Public domain | W3C validator |