![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-rn | Structured version Visualization version GIF version |
Description: Define the range of a class. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → ran 𝐹 = {6, 9} (ex-rn 30322). Contrast with domain (defined in df-dm 5688). For alternate definitions, see dfrn2 5891, dfrn3 5892, and dfrn4 6208. The notation "ran " is used by Enderton. The range of a function is often also called "the image of the function" (see definition in [Lang] p. ix), which can be justified by imadmrn 6074. Not to be confused with "codomain" (see df-f 6553), which may be a superset/superclass of the range (see frn 6730). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | crn 5679 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5677 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5678 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1533 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5891 dmcnvcnv 5935 rncnvcnv 5936 rneq 5938 rnss 5941 brelrng 5943 nfrn 5954 rncoss 5975 rncoeq 5978 cnvimarndm 6087 rnun 6152 rnin 6153 rnxp 6176 rnxpss 6178 imainrect 6187 rnsnopg 6227 cnvssrndm 6277 unidmrn 6285 dfdm2 6287 funcnvpr 6616 funcnvtp 6617 funcnvqp 6618 fncnv 6627 funcnvres 6632 funimacnv 6635 fimacnvdisj 6775 dff1o4 6846 foimacnv 6855 funcocnv2 6863 f1ompt 7120 nvof1o 7289 cnvexg 7932 tz7.48-3 8465 errn 8747 omxpenlem 9098 sbthlem5 9112 sbthlem8 9115 sbthlem9 9116 fodomr 9153 domss2 9161 rnfi 9361 zorn2lem4 10524 rnct 10550 fpwwe2lem12 10667 trclublem 14978 relexpcnv 15018 relexpnnrn 15028 invf 17754 cicsym 17790 cnvtsr 18583 znleval 21505 ordtbas2 23139 ordtcnv 23149 ordtrest2 23152 cnconn 23370 tgqtop 23660 adj1o 31776 fcoinver 32473 fresf1o 32497 fcnvgreu 32540 dfcnv2 32543 preiman0 32571 gsumhashmul 32860 cycpmfvlem 32925 cycpmfv1 32926 cycpmfv2 32927 cycpmfv3 32928 cycpmrn 32956 cnvordtrestixx 33645 xrge0iifhmeo 33668 mbfmcst 34010 0rrv 34202 elrn3 35487 dfrn6 37904 cnvresrn 37950 dmcoss2 38056 cnvrcl0 43197 conrel2d 43236 relexpaddss 43290 rntrclfvRP 43303 ntrneifv2 43652 |
Copyright terms: Public domain | W3C validator |