![]() |
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 7746 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7746 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun2 4171 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5973 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3986 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5324 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
7 | 5, 6 | mpan 688 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Vcvv 3461 ∪ cun 3942 ⊆ wss 3944 ∪ cuni 4909 dom cdm 5678 ran crn 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-cnv 5686 df-dm 5688 df-rn 5689 |
This theorem is referenced by: rnex 7918 imaexg 7921 rnexd 7923 xpexr 7926 xpexr2 7927 soex 7929 cnvexg 7932 coexg 7937 cofunexg 7953 funrnex 7958 abrexexgOLD 7966 tposexg 8246 iunon 8360 onoviun 8364 tz7.44lem1 8426 tz7.44-3 8429 fopwdom 9105 disjen 9159 domss2 9161 domssex 9163 hartogslem2 9568 ttrclexg 9748 djuexb 9934 dfac12lem2 10169 unirnfdomd 10592 hashimarn 14435 trclexlem 14977 relexp0g 15005 relexpsucnnr 15008 restval 17411 prdsbas 17442 prdsplusg 17443 prdsmulr 17444 prdsvsca 17445 prdshom 17452 sscpwex 17801 sylow1lem4 19568 sylow3lem2 19595 sylow3lem3 19596 lsmvalx 19606 txindislem 23581 xkoptsub 23602 fmfnfmlem3 23904 fmfnfmlem4 23905 ustuqtoplem 24188 ustuqtop0 24189 utopsnneiplem 24196 efabl 26529 efsubm 26530 addsuniflem 27964 ssltmul1 28097 ssltmul2 28098 precsexlem11 28165 perpln1 28586 perpln2 28587 isperp 28588 lmif 28661 islmib 28663 isgrpo 30379 grpoinvfval 30404 grpodivfval 30416 isvcOLD 30461 isnv 30494 abrexexd 32382 acunirnmpt 32526 acunirnmpt2 32527 acunirnmpt2f 32528 fnpreimac 32538 locfinreflem 33572 esumrnmpt2 33818 sxsigon 33942 omssubadd 34051 carsgclctunlem2 34070 pmeasadd 34076 sitgclg 34093 bnj1366 34591 ptrest 37223 elghomlem1OLD 37489 elghomlem2OLD 37490 isrngod 37502 iscringd 37602 imaexALTV 37932 xrnresex 38008 dfcnvrefrels2 38130 dfcnvrefrels3 38131 sticksstones3 41751 lmhmlnmsplit 42653 rclexi 43187 rtrclexlem 43188 trclubgNEW 43190 cnvrcl0 43197 dfrtrcl5 43201 relexpmulg 43282 relexp01min 43285 relexpxpmin 43289 unirnmap 44720 unirnmapsn 44726 ssmapsn 44728 fourierdlem70 45702 fourierdlem71 45703 fourierdlem80 45712 meadjiunlem 45991 omeiunle 46043 fexafv2ex 46738 |
Copyright terms: Public domain | W3C validator |