![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ressxr | Structured version Unicode version |
Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
ressxr |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 3620 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-xr 9526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseqtr4i 3490 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-v 3073 df-un 3434 df-in 3436 df-ss 3443 df-xr 9526 |
This theorem is referenced by: rexpssxrxp 9532 rexr 9533 0xr 9534 rexrd 9537 ltrelxr 9542 supxrre 11394 supxrbnd 11395 supxrgtmnf 11396 supxrre1 11397 supxrre2 11398 infmxrre 11402 iooval2 11437 fzval2 11550 uzsup 11812 hashxrcl 12237 seqcoll 12327 limsupval2 13069 limsupgre 13070 limsupbnd2 13072 rlimuni 13139 rlimcld2 13167 rlimno1 13242 isercolllem2 13254 isercoll 13256 caucvgrlem 13261 summolem2a 13303 ramtlecl 14172 ramxrcl 14189 ismet2 20033 prdsmet 20070 qtopbas 20463 tgqioo 20502 re2ndc 20503 xrsmopn 20514 metdcn2 20541 metdscn2 20558 bndth 20655 ovolunlem1a 21104 ovolunlem1 21105 ovoliunlem1 21110 ovoliun 21113 ovolicc2lem4 21128 voliunlem2 21158 voliunlem3 21159 opnmblALT 21209 vitalilem4 21217 mbfimaopnlem 21259 itg2le 21343 itg2seq 21346 dvfsumrlim 21629 itgsubst 21647 mdegleb 21661 mdeglt 21662 mdegldg 21663 mdegxrcl 21664 mdegcl 21666 mdegaddle 21671 mdegmullem 21675 deg1mul3le 21714 ig1pdvds 21774 aannenlem2 21921 taylfval 21950 radcnvcl 22008 radcnvlt1 22009 radcnvle 22011 xrlimcnp 22488 nmoxr 24311 nmooge0 24312 nmoolb 24316 nmoubi 24317 nmlno0lem 24338 nmopxr 25415 nmfnxr 25428 nmoplb 25456 nmopub 25457 nmfnlb 25473 nmfnleub 25474 nmlnop0iALT 25544 nmopun 25563 branmfn 25654 pjnmopi 25697 xlt2addrd 26195 xreceu 26235 rexdiv 26239 xrsmulgzz 26277 esumcst 26652 signsply0 27089 prodmolem2a 27584 mblfinlem2 28570 itg2addnc 28587 prdsbnd 28833 rrnequiv 28875 hbtlem2 29621 |
Copyright terms: Public domain | W3C validator |