![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexrd | GIF 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 7991 | . 2 ⊢ ℝ ⊆ ℝ* | |
2 | rexrd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | 1, 2 | sselid 3153 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ℝcr 7801 ℝ*cxr 7981 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-in 3135 df-ss 3142 df-xr 7986 |
This theorem is referenced by: xnn0xr 9233 rpxr 9648 rpxrd 9684 xnn0dcle 9789 xnegcl 9819 xaddf 9831 xaddval 9832 xnn0lenn0nn0 9852 xposdif 9869 iooshf 9939 icoshftf1o 9978 ioo0 10246 ioom 10247 ico0 10248 ioc0 10249 modqelico 10320 mulqaddmodid 10350 addmodid 10358 elicc4abs 11087 xrmaxiflemcl 11237 fprodge1 11631 pcxcl 12294 pcdvdsb 12302 pcaddlem 12321 pcadd 12322 xblss2ps 13571 xblss2 13572 blss2ps 13573 blss2 13574 blhalf 13575 cnblcld 13702 ioo2blex 13711 tgioo 13713 cnopnap 13761 suplociccreex 13769 suplociccex 13770 dedekindicc 13778 ivthinclemlm 13779 ivthinclemum 13780 ivthinclemlopn 13781 ivthinclemuopn 13783 ivthdec 13789 sin0pilem2 13870 pilem3 13871 |
Copyright terms: Public domain | W3C validator |