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 6853 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 6853 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun2 3739 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5305 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3577 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 4732 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
7 | 5, 6 | mpan 702 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 ⊆ wss 3540 ∪ cuni 4372 dom cdm 5038 ran crn 5039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-cnv 5046 df-dm 5048 df-rn 5049 |
This theorem is referenced by: rnex 6992 imaexg 6995 xpexr 6999 xpexr2 7000 soex 7002 cnvexg 7005 coexg 7010 cofunexg 7023 funrnex 7026 abrexexg 7034 tposexg 7253 iunon 7323 onoviun 7327 tz7.44lem1 7388 tz7.44-3 7391 fopwdom 7953 disjen 8002 domss2 8004 domssex 8006 hartogslem2 8331 dfac12lem2 8849 unirnfdomd 9268 focdmex 13001 hashf1rnOLD 13005 hashimarn 13085 trclexlem 13581 relexp0g 13610 relexpsucnnr 13613 restval 15910 prdsbas 15940 prdsplusg 15941 prdsmulr 15942 prdsvsca 15943 prdshom 15950 sscpwex 16298 sylow1lem4 17839 sylow3lem2 17866 sylow3lem3 17867 lsmvalx 17877 txindislem 21246 xkoptsub 21267 fmfnfmlem3 21570 fmfnfmlem4 21571 ustuqtoplem 21853 ustuqtop0 21854 utopsnneiplem 21861 efabl 24100 efsubm 24101 perpln1 25405 perpln2 25406 isperp 25407 lmif 25477 islmib 25479 sizeusglecusg 26014 isgrpo 26735 grpoinvfval 26760 grpodivfval 26772 isvcOLD 26818 isnv 26851 abrexexd 28731 acunirnmpt 28841 acunirnmpt2 28842 acunirnmpt2f 28843 locfinreflem 29235 esumrnmpt2 29457 sxsigon 29582 omssubadd 29689 carsgclctunlem2 29708 pmeasadd 29714 sitgclg 29731 bnj1366 30154 ptrest 32578 elghomlem1OLD 32854 elghomlem2OLD 32855 isrngod 32867 iscringd 32967 lmhmlnmsplit 36675 rclexi 36941 rtrclexlem 36942 trclubgNEW 36944 cnvrcl0 36951 dfrtrcl5 36955 relexpmulg 37021 relexp01min 37024 relexpxpmin 37028 unirnmap 38395 unirnmapsn 38401 ssmapsn 38403 fourierdlem70 39069 fourierdlem71 39070 fourierdlem80 39079 meadjiunlem 39358 omeiunle 39407 |
Copyright terms: Public domain | W3C validator |