| 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 30459). Contrast with domain (defined in df-dm 5695). For alternate definitions, see dfrn2 5899, dfrn3 5900, and dfrn4 6222. 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 6088. Not to be confused with "codomain" (see df-f 6565), which may be a superset/superclass of the range (see frn 6743). (Contributed by NM, 1-Aug-1994.) |
| Ref | Expression |
|---|---|
| df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | crn 5686 | . 2 class ran 𝐴 |
| 3 | 1 | ccnv 5684 | . . 3 class ◡𝐴 |
| 4 | 3 | cdm 5685 | . 2 class dom ◡𝐴 |
| 5 | 2, 4 | wceq 1540 | 1 wff ran 𝐴 = dom ◡𝐴 |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfrn2 5899 dmcnvcnv 5944 rncnvcnv 5945 rneq 5947 rnss 5950 brelrng 5952 nfrn 5963 rncoss 5986 rncoeq 5990 cnvimarndm 6101 rnun 6165 rnin 6166 rnxp 6190 rnxpss 6192 imainrect 6201 rnsnopg 6241 cnvssrndm 6291 unidmrn 6299 dfdm2 6301 funcnvpr 6628 funcnvtp 6629 funcnvqp 6630 fncnv 6639 funcnvres 6644 funimacnv 6647 fimacnvdisj 6786 dff1o4 6856 foimacnv 6865 funcocnv2 6873 f1ompt 7131 nvof1o 7300 cnvexg 7946 tz7.48-3 8484 errn 8767 omxpenlem 9113 sbthlem5 9127 sbthlem8 9130 sbthlem9 9131 fodomr 9168 domss2 9176 fodomfir 9368 rnfi 9380 zorn2lem4 10539 rnct 10565 fpwwe2lem12 10682 trclublem 15034 relexpcnv 15074 relexpnnrn 15084 invf 17812 cicsym 17848 cnvtsr 18633 znleval 21573 ordtbas2 23199 ordtcnv 23209 ordtrest2 23212 cnconn 23430 tgqtop 23720 adj1o 31913 fcoinver 32617 fresf1o 32641 fcnvgreu 32683 dfcnv2 32686 preiman0 32719 gsumhashmul 33064 cycpmfvlem 33132 cycpmfv1 33133 cycpmfv2 33134 cycpmfv3 33135 cycpmrn 33163 cnvordtrestixx 33912 xrge0iifhmeo 33935 mbfmcst 34261 0rrv 34453 elrn3 35762 dfrn6 38303 cnvresrn 38349 dmcoss2 38455 cnvrcl0 43638 conrel2d 43677 relexpaddss 43731 rntrclfvRP 43744 ntrneifv2 44093 |
| Copyright terms: Public domain | W3C validator |