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 28547). Contrast with domain (defined in df-dm 5576). For alternate definitions, see dfrn2 5772, dfrn3 5773, and dfrn4 6080. 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 5954. Not to be confused with "codomain" (see df-f 6402), which may be a superset/superclass of the range (see frn 6571). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | crn 5567 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5565 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5566 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1543 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5772 dmcnvcnv 5817 rncnvcnv 5818 rneq 5820 rnss 5823 brelrng 5825 nfrn 5836 rncoss 5856 rncoeq 5859 cnvimarndm 5965 rnun 6024 rnin 6025 rnxp 6048 rnxpss 6050 imainrect 6059 rnsnopg 6099 cnvssrndm 6149 unidmrn 6157 dfdm2 6159 funcnvpr 6460 funcnvtp 6461 funcnvqp 6462 fncnv 6471 funcnvres 6476 funimacnv 6479 fimacnvdisj 6616 dff1o4 6688 foimacnv 6697 funcocnv2 6704 f1ompt 6947 nvof1o 7110 cnvexg 7721 tz7.48-3 8201 errn 8434 omxpenlem 8769 sbthlem5 8783 sbthlem8 8786 sbthlem9 8787 fodomr 8820 domss2 8828 rnfi 8984 zorn2lem4 10138 rnct 10164 fpwwe2lem12 10281 trclublem 14583 relexpcnv 14623 relexpnnrn 14633 invf 17298 cicsym 17334 cnvtsr 18119 znleval 20544 ordtbas2 22112 ordtcnv 22122 ordtrest2 22125 cnconn 22343 tgqtop 22633 adj1o 29999 fcoinver 30689 fresf1o 30709 fcnvgreu 30754 dfcnv2 30757 preiman0 30786 gsumhashmul 31059 cycpmfvlem 31122 cycpmfv1 31123 cycpmfv2 31124 cycpmfv3 31125 cycpmrn 31153 cnvordtrestixx 31601 xrge0iifhmeo 31624 mbfmcst 31962 0rrv 32154 elrn3 33471 dfrn6 36202 cnvresrn 36247 dmcoss2 36336 cnvrcl0 40938 conrel2d 40978 relexpaddss 41032 rntrclfvRP 41045 ntrneifv2 41396 |
Copyright terms: Public domain | W3C validator |