Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexrd | Unicode version |
Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rexrd.1 |
Ref | Expression |
---|---|
rexrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 7777 | . 2 | |
2 | rexrd.1 | . 2 | |
3 | 1, 2 | sseldi 3065 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cr 7587 cxr 7767 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-un 3045 df-in 3047 df-ss 3054 df-xr 7772 |
This theorem is referenced by: xnn0xr 9013 rpxr 9417 rpxrd 9452 xnegcl 9583 xaddf 9595 xaddval 9596 xnn0lenn0nn0 9616 xposdif 9633 iooshf 9703 icoshftf1o 9742 ioo0 10005 ioom 10006 ico0 10007 ioc0 10008 modqelico 10075 mulqaddmodid 10105 addmodid 10113 elicc4abs 10834 xrmaxiflemcl 10982 xblss2ps 12500 xblss2 12501 blss2ps 12502 blss2 12503 blhalf 12504 cnblcld 12631 ioo2blex 12640 tgioo 12642 cnopnap 12690 suplociccreex 12698 suplociccex 12699 dedekindicc 12707 ivthinclemlm 12708 ivthinclemum 12709 ivthinclemlopn 12710 ivthinclemuopn 12712 ivthdec 12718 sin0pilem2 12790 pilem3 12791 |
Copyright terms: Public domain | W3C validator |