![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnexg | 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, 31-Mar-1995.) |
Ref | Expression |
---|---|
rnexg | ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexg 7215 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7215 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun2 4004 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5617 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3836 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5029 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
7 | 5, 6 | mpan 681 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2164 Vcvv 3414 ∪ cun 3796 ⊆ wss 3798 ∪ cuni 4658 dom cdm 5342 ran crn 5343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 ax-un 7209 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-cnv 5350 df-dm 5352 df-rn 5353 |
This theorem is referenced by: rnex 7362 imaexg 7365 xpexr 7368 xpexr2 7369 soex 7371 cnvexg 7374 coexg 7379 cofunexg 7392 funrnex 7395 abrexexg 7402 tposexg 7631 iunon 7702 onoviun 7706 tz7.44lem1 7767 tz7.44-3 7770 fopwdom 8337 disjen 8386 domss2 8388 domssex 8390 hartogslem2 8717 dfac12lem2 9281 unirnfdomd 9704 focdmex 13431 hashimarn 13516 trclexlem 14112 relexp0g 14139 relexpsucnnr 14142 restval 16440 prdsbas 16470 prdsplusg 16471 prdsmulr 16472 prdsvsca 16473 prdshom 16480 sscpwex 16827 sylow1lem4 18367 sylow3lem2 18394 sylow3lem3 18395 lsmvalx 18405 txindislem 21807 xkoptsub 21828 fmfnfmlem3 22130 fmfnfmlem4 22131 ustuqtoplem 22413 ustuqtop0 22414 utopsnneiplem 22421 efabl 24696 efsubm 24697 perpln1 26022 perpln2 26023 isperp 26024 lmif 26094 islmib 26096 isgrpo 27896 grpoinvfval 27921 grpodivfval 27933 isvcOLD 27978 isnv 28011 abrexexd 29884 acunirnmpt 29997 acunirnmpt2 29998 acunirnmpt2f 29999 locfinreflem 30441 esumrnmpt2 30664 sxsigon 30789 omssubadd 30896 carsgclctunlem2 30915 pmeasadd 30921 sitgclg 30938 bnj1366 31435 ptrest 33945 elghomlem1OLD 34219 elghomlem2OLD 34220 isrngod 34232 iscringd 34332 xrnresex 34705 dfcnvrefrels2 34817 dfcnvrefrels3 34818 lmhmlnmsplit 38493 rclexi 38756 rtrclexlem 38757 trclubgNEW 38759 cnvrcl0 38766 dfrtrcl5 38770 relexpmulg 38836 relexp01min 38839 relexpxpmin 38843 unirnmap 40199 unirnmapsn 40205 ssmapsn 40207 fourierdlem70 41180 fourierdlem71 41181 fourierdlem80 41190 meadjiunlem 41466 omeiunle 41518 fexafv2ex 42115 |
Copyright terms: Public domain | W3C validator |