![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexr | GIF version |
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
rexr | ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 7681 | . 2 ⊢ ℝ ⊆ ℝ* | |
2 | 1 | sseli 3043 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ℝcr 7499 ℝ*cxr 7671 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-un 3025 df-in 3027 df-ss 3034 df-xr 7676 |
This theorem is referenced by: rexri 7695 lenlt 7711 ltpnf 9408 mnflt 9410 xrltnsym 9420 xrlttr 9422 xrltso 9423 xrre 9444 xrre3 9446 xltnegi 9459 rexadd 9476 xaddnemnf 9481 xaddnepnf 9482 xaddcom 9485 xnegdi 9492 xpncan 9495 xnpcan 9496 xleadd1a 9497 xleadd1 9499 xltadd1 9500 xltadd2 9501 xsubge0 9505 xposdif 9506 elioo4g 9558 elioc2 9560 elico2 9561 elicc2 9562 iccss 9565 iooshf 9576 iooneg 9612 icoshft 9614 qbtwnxr 9876 modqmuladdim 9981 elicc4abs 10706 icodiamlt 10792 xrmaxrecl 10863 xrmaxaddlem 10868 xrminrecl 10881 bl2in 12331 blssps 12355 blss 12356 bl2ioo 12461 blssioo 12464 |
Copyright terms: Public domain | W3C validator |