Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rnex | Structured version Visualization version Unicode version |
Description: The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.) |
Ref | Expression |
---|---|
dmex.1 |
Ref | Expression |
---|---|
rnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmex.1 | . 2 | |
2 | rnexg 7098 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 cvv 3200 crn 5115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-cnv 5122 df-dm 5124 df-rn 5125 |
This theorem is referenced by: elxp4 7110 elxp5 7111 ffoss 7127 fvclex 7138 abrexexOLD 7142 wemoiso2 7154 2ndval 7171 fo2nd 7189 ixpsnf1o 7948 bren 7964 mapen 8124 ssenen 8134 sucdom2 8156 fodomfib 8240 hartogslem1 8447 brwdom 8472 unxpwdom2 8493 noinfep 8557 r0weon 8835 fseqen 8850 acnlem 8871 infpwfien 8885 aceq3lem 8943 dfac4 8945 dfac5 8951 dfac2 8953 dfac9 8958 dfac12lem2 8966 dfac12lem3 8967 infmap2 9040 cfflb 9081 infpssr 9130 fin23lem14 9155 fin23lem16 9157 fin23lem17 9160 fin23lem38 9171 fin23lem39 9172 axdc2lem 9270 axdc3lem2 9273 axcclem 9279 ttukeylem6 9336 wunex2 9560 wuncval2 9569 intgru 9636 wfgru 9638 qexALT 11803 hashfacen 13238 shftfval 13810 vdwapval 15677 restfn 16085 prdsval 16115 wunfunc 16559 wunnat 16616 arwval 16693 catcfuccl 16759 catcxpccl 16847 yon11 16904 yon12 16905 yon2 16906 yonpropd 16908 oppcyon 16909 yonffth 16924 yoniso 16925 plusffval 17247 sylow1lem2 18014 sylow2blem1 18035 sylow2blem2 18036 sylow3lem1 18042 sylow3lem6 18047 dmdprd 18397 dprdval 18402 staffval 18847 scaffval 18881 lpival 19245 ipffval 19993 cmpsub 21203 2ndcsep 21262 1stckgen 21357 kgencn2 21360 txcmplem1 21444 blbas 22235 met1stc 22326 psmetutop 22372 nmfval 22393 qtopbaslem 22562 dchrptlem2 24990 dchrptlem3 24991 ishpg 25651 edgval 25941 edgvalOLD 25942 bafval 27459 vsfval 27488 foresf1o 29343 locfinreflem 29907 cmpcref 29917 ordtconnlem1 29970 qqhval 30018 sigapildsys 30225 dya2icoseg2 30340 dya2iocuni 30345 sxbrsigalem2 30348 sxbrsigalem5 30350 omssubadd 30362 mvtval 31397 mvrsval 31402 mstaval 31441 trpredex 31737 brrestrict 32056 relowlssretop 33211 lindsdom 33403 indexdom 33529 heiborlem1 33610 isdrngo2 33757 isrngohom 33764 idlval 33812 isidl 33813 igenval 33860 lsatset 34277 dicval 36465 trclexi 37927 rtrclexi 37928 dfrtrcl5 37936 dfrcl2 37966 stoweidlem59 40276 fourierdlem71 40394 salgensscntex 40562 aacllem 42547 |
Copyright terms: Public domain | W3C validator |