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 7602 | . 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3495 ran crn 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-cnv 5557 df-dm 5559 df-rn 5560 |
This theorem is referenced by: elxp4 7615 elxp5 7616 ffoss 7638 fvclex 7651 wemoiso2 7666 2ndval 7683 fo2nd 7701 ixpsnf1o 8491 bren 8507 mapen 8670 ssenen 8680 sucdom2 8703 fodomfib 8787 hartogslem1 8995 brwdom 9020 unxpwdom2 9041 noinfep 9112 r0weon 9427 fseqen 9442 acnlem 9463 infpwfien 9477 aceq3lem 9535 dfac4 9537 dfac5 9543 dfac2b 9545 dfac9 9551 dfac12lem2 9559 dfac12lem3 9560 infmap2 9629 cfflb 9670 infpssr 9719 fin23lem14 9744 fin23lem16 9746 fin23lem17 9749 fin23lem38 9760 fin23lem39 9761 axdc2lem 9859 axdc3lem2 9862 axcclem 9868 ttukeylem6 9925 wunex2 10149 wuncval2 10158 intgru 10225 wfgru 10227 qexALT 12353 seqexw 13375 hashfacen 13802 shftfval 14419 vdwapval 16299 restfn 16688 prdsval 16718 wunfunc 17159 wunnat 17216 arwval 17293 catcfuccl 17359 catcxpccl 17447 yon11 17504 yon12 17505 yon2 17506 yonpropd 17508 oppcyon 17509 yonffth 17524 yoniso 17525 plusffval 17848 grpsubfval 18087 mulgfval 18166 sylow1lem2 18655 sylow2blem1 18676 sylow2blem2 18677 sylow3lem1 18683 sylow3lem6 18688 dmdprd 19051 dprdval 19056 staffval 19549 scaffval 19583 lpival 19948 ipffval 20722 cmpsub 21938 2ndcsep 21997 1stckgen 22092 kgencn2 22095 txcmplem1 22179 blbas 22969 met1stc 23060 psmetutop 23106 nmfval 23127 dchrptlem2 25769 dchrptlem3 25770 ishpg 26473 edgval 26762 bafval 28309 vsfval 28338 foresf1o 30193 fnpreimac 30345 locfinreflem 31004 cmpcref 31014 ordtconnlem1 31067 qqhval 31115 sigapildsys 31321 dya2icoseg2 31436 dya2iocuni 31441 sxbrsigalem2 31444 sxbrsigalem5 31446 omssubadd 31458 mvtval 32645 mvrsval 32650 mstaval 32689 trpredex 32974 brrestrict 33308 relowlssretop 34527 exrecfnlem 34543 ctbssinf 34570 lindsdom 34768 indexdom 34892 heiborlem1 34972 isdrngo2 35119 isrngohom 35126 idlval 35174 isidl 35175 igenval 35222 lsatset 36008 dicval 38194 trclexi 39860 rtrclexi 39861 dfrtrcl5 39869 dfrcl2 39899 stoweidlem59 42225 fourierdlem71 42343 salgensscntex 42508 aacllem 44800 |
Copyright terms: Public domain | W3C validator |