|   | 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 7925 | . 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ∈ V | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2107 Vcvv 3479 ran crn 5685 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 ax-un 7756 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-opab 5205 df-cnv 5692 df-dm 5694 df-rn 5695 | 
| This theorem is referenced by: elxp4 7945 elxp5 7946 ffoss 7971 fvclex 7984 wemoiso2 8000 2ndval 8018 fo2nd 8036 mapfoss 8893 ixpsnf1o 8979 bren 8996 sucdom2OLD 9123 mapen 9182 ssenen 9192 sucdom2 9244 fodomfib 9370 fodomfibOLD 9372 hartogslem1 9583 brwdom 9608 unxpwdom2 9629 noinfep 9701 r0weon 10053 fseqen 10068 acnlem 10089 infpwfien 10103 aceq3lem 10161 dfac4 10163 dfac5 10170 dfac2b 10172 dfac9 10178 dfac12lem2 10186 dfac12lem3 10187 infmap2 10258 cfflb 10300 infpssr 10349 fin23lem14 10374 fin23lem16 10376 fin23lem17 10379 fin23lem38 10390 fin23lem39 10391 axdc2lem 10489 axdc3lem2 10492 axcclem 10498 ttukeylem6 10555 wunex2 10779 wuncval2 10788 intgru 10855 wfgru 10857 qexALT 13007 seqexw 14059 shftfval 15110 vdwapval 17012 restfn 17470 prdsvallem 17500 prdsval 17501 wunfunc 17947 wunnat 18005 arwval 18089 catcfuccl 18164 catcxpccl 18253 yon11 18310 yon12 18311 yon2 18312 yonpropd 18314 oppcyon 18315 yonffth 18330 yoniso 18331 plusffval 18660 grpsubfval 19002 mulgfval 19088 sylow1lem2 19618 sylow2blem1 19639 sylow2blem2 19640 sylow3lem1 19646 sylow3lem6 19651 dmdprd 20019 dprdval 20024 staffval 20843 scaffval 20879 lpival 21335 ipffval 21667 cmpsub 23409 2ndcsep 23468 1stckgen 23563 kgencn2 23566 txcmplem1 23650 blbas 24441 met1stc 24535 psmetutop 24581 nmfval 24602 dchrptlem2 27310 dchrptlem3 27311 mulsproplem9 28151 ishpg 28768 edgval 29067 bafval 30624 vsfval 30653 foresf1o 32524 fnpreimac 32682 nsgmgc 33441 nsgqusf1o 33445 idlsrgtset 33537 locfinreflem 33840 cmpcref 33850 rspectopn 33867 ordtconnlem1 33924 qqhval 33974 sigapildsys 34164 dya2icoseg2 34281 dya2iocuni 34286 sxbrsigalem2 34289 sxbrsigalem5 34291 omssubadd 34303 mvtval 35506 mvrsval 35511 mstaval 35550 brrestrict 35951 relowlssretop 37365 exrecfnlem 37381 ctbssinf 37408 lindsdom 37622 indexdom 37742 heiborlem1 37819 isdrngo2 37966 isrngohom 37973 idlval 38021 isidl 38022 igenval 38069 lsatset 38992 dicval 41179 aks6d1c6isolem2 42177 prjcrvfval 42646 trclexi 43638 rtrclexi 43639 dfrtrcl5 43647 dfrcl2 43692 wfaxrep 45016 stoweidlem59 46079 fourierdlem71 46197 salgensscntex 46364 aacllem 49375 | 
| Copyright terms: Public domain | W3C validator |