![]() |
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 7678 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7678 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun2 4134 | . . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5926 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3954 | . . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5281 | . . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V) | |
7 | 5, 6 | mpan 689 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3444 ∪ cun 3909 ⊆ wss 3911 ∪ cuni 4866 dom cdm 5634 ran crn 5635 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-cnv 5642 df-dm 5644 df-rn 5645 |
This theorem is referenced by: rnex 7850 imaexg 7853 xpexr 7856 xpexr2 7857 soex 7859 cnvexg 7862 coexg 7867 cofunexg 7882 funrnex 7887 abrexexgOLD 7895 tposexg 8172 iunon 8286 onoviun 8290 tz7.44lem1 8352 tz7.44-3 8355 fopwdom 9027 disjen 9081 domss2 9083 domssex 9085 hartogslem2 9484 ttrclexg 9664 djuexb 9850 dfac12lem2 10085 unirnfdomd 10508 hashimarn 14346 trclexlem 14885 relexp0g 14913 relexpsucnnr 14916 restval 17313 prdsbas 17344 prdsplusg 17345 prdsmulr 17346 prdsvsca 17347 prdshom 17354 sscpwex 17703 sylow1lem4 19388 sylow3lem2 19415 sylow3lem3 19416 lsmvalx 19426 txindislem 23000 xkoptsub 23021 fmfnfmlem3 23323 fmfnfmlem4 23324 ustuqtoplem 23607 ustuqtop0 23608 utopsnneiplem 23615 efabl 25922 efsubm 25923 addsunif 27332 perpln1 27694 perpln2 27695 isperp 27696 lmif 27769 islmib 27771 isgrpo 29481 grpoinvfval 29506 grpodivfval 29518 isvcOLD 29563 isnv 29596 abrexexd 31478 acunirnmpt 31621 acunirnmpt2 31622 acunirnmpt2f 31623 fnpreimac 31633 rnexd 31641 locfinreflem 32478 esumrnmpt2 32724 sxsigon 32848 omssubadd 32957 carsgclctunlem2 32976 pmeasadd 32982 sitgclg 32999 bnj1366 33498 ptrest 36123 elghomlem1OLD 36390 elghomlem2OLD 36391 isrngod 36403 iscringd 36503 imaexALTV 36837 xrnresex 36914 dfcnvrefrels2 37036 dfcnvrefrels3 37037 sticksstones3 40602 lmhmlnmsplit 41457 rclexi 41975 rtrclexlem 41976 trclubgNEW 41978 cnvrcl0 41985 dfrtrcl5 41989 relexpmulg 42070 relexp01min 42073 relexpxpmin 42077 unirnmap 43516 unirnmapsn 43522 ssmapsn 43524 fourierdlem70 44503 fourierdlem71 44504 fourierdlem80 44513 meadjiunlem 44792 omeiunle 44844 fexafv2ex 45538 |
Copyright terms: Public domain | W3C validator |