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 7617 | . 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 Vcvv 3497 ran crn 5559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 ax-un 7464 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-opab 5132 df-cnv 5566 df-dm 5568 df-rn 5569 |
This theorem is referenced by: elxp4 7630 elxp5 7631 ffoss 7650 fvclex 7663 wemoiso2 7678 2ndval 7695 fo2nd 7713 ixpsnf1o 8505 bren 8521 mapen 8684 ssenen 8694 sucdom2 8717 fodomfib 8801 hartogslem1 9009 brwdom 9034 unxpwdom2 9055 noinfep 9126 r0weon 9441 fseqen 9456 acnlem 9477 infpwfien 9491 aceq3lem 9549 dfac4 9551 dfac5 9557 dfac2b 9559 dfac9 9565 dfac12lem2 9573 dfac12lem3 9574 infmap2 9643 cfflb 9684 infpssr 9733 fin23lem14 9758 fin23lem16 9760 fin23lem17 9763 fin23lem38 9774 fin23lem39 9775 axdc2lem 9873 axdc3lem2 9876 axcclem 9882 ttukeylem6 9939 wunex2 10163 wuncval2 10172 intgru 10239 wfgru 10241 qexALT 12366 seqexw 13388 hashfacen 13815 shftfval 14432 vdwapval 16312 restfn 16701 prdsval 16731 wunfunc 17172 wunnat 17229 arwval 17306 catcfuccl 17372 catcxpccl 17460 yon11 17517 yon12 17518 yon2 17519 yonpropd 17521 oppcyon 17522 yonffth 17537 yoniso 17538 plusffval 17861 grpsubfval 18150 mulgfval 18229 sylow1lem2 18727 sylow2blem1 18748 sylow2blem2 18749 sylow3lem1 18755 sylow3lem6 18760 dmdprd 19123 dprdval 19128 staffval 19621 scaffval 19655 lpival 20021 ipffval 20795 cmpsub 22011 2ndcsep 22070 1stckgen 22165 kgencn2 22168 txcmplem1 22252 blbas 23043 met1stc 23134 psmetutop 23180 nmfval 23201 dchrptlem2 25844 dchrptlem3 25845 ishpg 26548 edgval 26837 bafval 28384 vsfval 28413 foresf1o 30268 fnpreimac 30419 locfinreflem 31108 cmpcref 31118 ordtconnlem1 31171 qqhval 31219 sigapildsys 31425 dya2icoseg2 31540 dya2iocuni 31545 sxbrsigalem2 31548 sxbrsigalem5 31550 omssubadd 31562 mvtval 32751 mvrsval 32756 mstaval 32795 trpredex 33080 brrestrict 33414 relowlssretop 34648 exrecfnlem 34664 ctbssinf 34691 lindsdom 34890 indexdom 35013 heiborlem1 35093 isdrngo2 35240 isrngohom 35247 idlval 35295 isidl 35296 igenval 35343 lsatset 36130 dicval 38316 trclexi 39986 rtrclexi 39987 dfrtrcl5 39995 dfrcl2 40025 stoweidlem59 42351 fourierdlem71 42469 salgensscntex 42634 aacllem 44909 |
Copyright terms: Public domain | W3C validator |