| 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 7739 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
| 2 | uniexg 7739 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
| 3 | ssun2 4140 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
| 4 | dmrnssfld 5965 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
| 5 | 3, 4 | sstri 3954 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
| 6 | ssexg 5294 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
| 7 | 5, 6 | mpan 702 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
| 8 | 1, 2, 7 | 3syl 19 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2149 Vcvv 3463 ∪ cun 3911 ⊆ wss 3913 ∪ cuni 4876 dom cdm 5662 ran crn 5663 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 ax-sep 5261 ax-pr 5405 ax-un 7733 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-cnv 5670 df-dm 5672 df-rn 5673 |
| This theorem is referenced by: rnex 7907 imaexg 7910 rnexd 7912 xpexr 7915 xpexr2 7916 soex 7918 cnvexg 7921 coexg 7926 cofunexg 7946 funrnex 7951 tposexg 8236 iunon 8326 onoviun 8330 tz7.44lem1 8392 tz7.44-3 8395 fopwdom 9073 disjen 9122 domss2 9124 domssex 9126 hartogslem2 9505 ttrclexg 9692 djuexb 9895 dfac12lem2 10128 unirnfdomd 10552 hashimarn 14477 trclexlem 15031 relexp0g 15059 relexpsucnnr 15062 restval 17479 prdsbas 17510 prdsplusg 17511 prdsmulr 17512 prdsvsca 17513 prdshom 17520 sscpwex 17872 sylow1lem4 19671 sylow3lem2 19698 sylow3lem3 19699 lsmvalx 19709 txindislem 23759 xkoptsub 23780 fmfnfmlem3 24082 fmfnfmlem4 24083 ustuqtoplem 24365 ustuqtop0 24366 utopsnneiplem 24373 efabl 26681 efsubm 26682 addsuniflem 28160 sltmuls1 28306 sltmuls2 28307 precsexlem11 28376 perpln1 28949 perpln2 28950 isperp 28951 lmif 29052 islmib 29054 isgrpo 30790 grpoinvfval 30815 grpodivfval 30827 isvcOLD 30872 isnv 30905 abrexexd 32796 acunirnmpt 32945 acunirnmpt2 32946 acunirnmpt2f 32947 fnpreimac 32956 locfinreflem 34175 esumrnmpt2 34403 sxsigon 34527 omssubadd 34635 carsgclctunlem2 34654 pmeasadd 34660 sitgclg 34677 bnj1366 35162 ptrest 38158 elghomlem1OLD 38424 elghomlem2OLD 38425 isrngod 38437 iscringd 38537 xrnresex 38968 dfcnvrefrels2 39147 dfcnvrefrels3 39148 eldisjs7 39480 sticksstones3 42805 lmhmlnmsplit 43706 rclexi 44233 rtrclexlem 44234 trclubgNEW 44236 cnvrcl0 44243 dfrtrcl5 44247 relexpmulg 44328 relexp01min 44331 relexpxpmin 44335 unirnmap 45816 unirnmapsn 45822 ssmapsn 45824 fourierdlem70 46782 fourierdlem71 46783 fourierdlem80 46792 meadjiunlem 47071 omeiunle 47123 fexafv2ex 47846 |
| Copyright terms: Public domain | W3C validator |