![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnex | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
rnex | ⊢ ran 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | rnexg 7891 | . 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3474 ran crn 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7721 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-cnv 5683 df-dm 5685 df-rn 5686 |
This theorem is referenced by: elxp4 7909 elxp5 7910 ffoss 7928 fvclex 7941 wemoiso2 7957 2ndval 7974 fo2nd 7992 mapfoss 8842 ixpsnf1o 8928 bren 8945 brenOLD 8946 sucdom2OLD 9078 mapen 9137 ssenen 9147 sucdom2 9202 fodomfib 9322 hartogslem1 9533 brwdom 9558 unxpwdom2 9579 noinfep 9651 r0weon 10003 fseqen 10018 acnlem 10039 infpwfien 10053 aceq3lem 10111 dfac4 10113 dfac5 10119 dfac2b 10121 dfac9 10127 dfac12lem2 10135 dfac12lem3 10136 infmap2 10209 cfflb 10250 infpssr 10299 fin23lem14 10324 fin23lem16 10326 fin23lem17 10329 fin23lem38 10340 fin23lem39 10341 axdc2lem 10439 axdc3lem2 10442 axcclem 10448 ttukeylem6 10505 wunex2 10729 wuncval2 10738 intgru 10805 wfgru 10807 qexALT 12944 seqexw 13978 hashfacenOLD 14410 shftfval 15013 vdwapval 16902 restfn 17366 prdsvallem 17396 prdsval 17397 wunfunc 17845 wunfuncOLD 17846 wunnat 17903 wunnatOLD 17904 arwval 17989 catcfuccl 18065 catcfucclOLD 18066 catcxpccl 18155 catcxpcclOLD 18156 yon11 18213 yon12 18214 yon2 18215 yonpropd 18217 oppcyon 18218 yonffth 18233 yoniso 18234 plusffval 18563 grpsubfval 18864 mulgfval 18946 sylow1lem2 19461 sylow2blem1 19482 sylow2blem2 19483 sylow3lem1 19489 sylow3lem6 19494 dmdprd 19862 dprdval 19867 staffval 20447 scaffval 20482 lpival 20875 ipffval 21192 cmpsub 22895 2ndcsep 22954 1stckgen 23049 kgencn2 23052 txcmplem1 23136 blbas 23927 met1stc 24021 psmetutop 24067 nmfval 24088 dchrptlem2 26757 dchrptlem3 26758 mulsproplem9 27569 ishpg 27999 edgval 28298 bafval 29844 vsfval 29873 foresf1o 31729 fnpreimac 31883 nsgmgc 32511 nsgqusf1o 32515 idlsrgtset 32610 locfinreflem 32808 cmpcref 32818 rspectopn 32835 ordtconnlem1 32892 qqhval 32942 sigapildsys 33148 dya2icoseg2 33265 dya2iocuni 33270 sxbrsigalem2 33273 sxbrsigalem5 33275 omssubadd 33287 mvtval 34479 mvrsval 34484 mstaval 34523 brrestrict 34909 relowlssretop 36232 exrecfnlem 36248 ctbssinf 36275 lindsdom 36470 indexdom 36590 heiborlem1 36667 isdrngo2 36814 isrngohom 36821 idlval 36869 isidl 36870 igenval 36917 lsatset 37848 dicval 40035 prjcrvfval 41369 trclexi 42356 rtrclexi 42357 dfrtrcl5 42365 dfrcl2 42410 stoweidlem59 44761 fourierdlem71 44879 salgensscntex 45046 aacllem 47801 |
Copyright terms: Public domain | W3C validator |