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 6955 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 6955 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun2 3777 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5384 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3612 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 4804 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
7 | 5, 6 | mpan 706 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 ∪ cuni 4436 dom cdm 5114 ran crn 5115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-cnv 5122 df-dm 5124 df-rn 5125 |
This theorem is referenced by: rnex 7100 imaexg 7103 xpexr 7106 xpexr2 7107 soex 7109 cnvexg 7112 coexg 7117 cofunexg 7130 funrnex 7133 abrexexg 7140 tposexg 7366 iunon 7436 onoviun 7440 tz7.44lem1 7501 tz7.44-3 7504 fopwdom 8068 disjen 8117 domss2 8119 domssex 8121 hartogslem2 8448 dfac12lem2 8966 unirnfdomd 9389 focdmex 13139 hashf1rnOLD 13143 hashimarn 13227 trclexlem 13733 relexp0g 13762 relexpsucnnr 13765 restval 16087 prdsbas 16117 prdsplusg 16118 prdsmulr 16119 prdsvsca 16120 prdshom 16127 sscpwex 16475 sylow1lem4 18016 sylow3lem2 18043 sylow3lem3 18044 lsmvalx 18054 txindislem 21436 xkoptsub 21457 fmfnfmlem3 21760 fmfnfmlem4 21761 ustuqtoplem 22043 ustuqtop0 22044 utopsnneiplem 22051 efabl 24296 efsubm 24297 perpln1 25605 perpln2 25606 isperp 25607 lmif 25677 islmib 25679 isgrpo 27351 grpoinvfval 27376 grpodivfval 27388 isvcOLD 27434 isnv 27467 abrexexd 29347 acunirnmpt 29459 acunirnmpt2 29460 acunirnmpt2f 29461 locfinreflem 29907 esumrnmpt2 30130 sxsigon 30255 omssubadd 30362 carsgclctunlem2 30381 pmeasadd 30387 sitgclg 30404 bnj1366 30900 ptrest 33408 elghomlem1OLD 33684 elghomlem2OLD 33685 isrngod 33697 iscringd 33797 lmhmlnmsplit 37657 rclexi 37922 rtrclexlem 37923 trclubgNEW 37925 cnvrcl0 37932 dfrtrcl5 37936 relexpmulg 38002 relexp01min 38005 relexpxpmin 38009 unirnmap 39400 unirnmapsn 39406 ssmapsn 39408 fourierdlem70 40393 fourierdlem71 40394 fourierdlem80 40403 meadjiunlem 40682 omeiunle 40731 |
Copyright terms: Public domain | W3C validator |