![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnexg | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexg 6593 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | uniexg 6593 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ssun2 3600 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dmrnssfld 5096 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sstri 3443 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | ssexg 4552 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | mpan 677 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | 3syl 18 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-cnv 4845 df-dm 4847 df-rn 4848 |
This theorem is referenced by: rnex 6732 imaexg 6735 xpexr 6738 xpexr2 6739 soex 6741 cnvexg 6744 coexg 6749 cofunexg 6762 funrnex 6765 abrexexg 6773 tposexg 6992 iunon 7062 onoviun 7067 tz7.44lem1 7128 tz7.44-3 7131 fopwdom 7685 disjen 7734 domss2 7736 domssex 7738 hartogslem2 8063 dfac12lem2 8579 unirnfdomd 8997 hashf1rn 12542 hashimarn 12617 trclexlem 13070 relexp0g 13097 relexpsucnnr 13100 restval 15337 prdsbas 15367 prdsplusg 15368 prdsmulr 15369 prdsvsca 15370 prdshom 15377 sscpwex 15732 sylow1lem4 17265 sylow3lem2 17292 sylow3lem3 17293 lsmvalx 17303 txindislem 20660 xkoptsub 20681 fmfnfmlem3 20983 fmfnfmlem4 20984 ustuqtoplem 21266 ustuqtop0 21267 utopsnneiplem 21274 efabl 23511 efsubm 23512 perpln1 24767 perpln2 24768 isperp 24769 lmif 24839 islmib 24841 sizeusglecusg 25226 isgrpo 25936 grpoinvfval 25964 grpodivfval 25982 gxfval 25997 issubgoi 26050 elghomlem1OLD 26101 elghomlem2OLD 26102 ghgrpOLD 26108 isrngod 26119 isvc 26212 isnv 26243 abrexexd 28155 acunirnmpt 28273 acunirnmpt2 28274 acunirnmpt2f 28275 locfinreflem 28679 esumrnmpt2 28901 sxsigon 29026 omssubadd 29140 omssubaddOLD 29144 carsgclctunlem2 29163 pmeasadd 29170 sitgclg 29187 bnj1366 29653 ptrest 31951 iscringd 32244 lmhmlnmsplit 35957 rclexi 36234 rtrclexlem 36235 trclubgNEW 36237 cnvrcl0 36244 dfrtrcl5 36248 relexpmulg 36314 relexp01min 36317 relexpxpmin 36321 fourierdlem70 38050 fourierdlem71 38051 fourierdlem80 38060 meadjiunlem 38313 omeiunle 38348 |
Copyright terms: Public domain | W3C validator |