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 28147). Contrast with domain (defined in df-dm 5559). For alternate definitions, see dfrn2 5753, dfrn3 5754, and dfrn4 6053. 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 5933. Not to be confused with "codomain" (see df-f 6353), which may be a superset/superclass of the range (see frn 6514). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | crn 5550 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5548 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5549 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1528 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5753 dmcnvcnv 5797 rncnvcnv 5798 rneq 5800 rnss 5803 brelrng 5805 nfrn 5818 rncoss 5837 rncoeq 5840 cnvimarndm 5944 rnun 5998 rnin 5999 rnxp 6021 rnxpss 6023 imainrect 6032 rnsnopg 6072 cnvssrndm 6116 unidmrn 6124 dfdm2 6126 funcnvpr 6410 funcnvtp 6411 funcnvqp 6412 fncnv 6421 funcnvres 6426 funimacnv 6429 fimacnvdisj 6551 dff1o4 6617 foimacnv 6626 funcocnv2 6633 f1ompt 6868 nvof1o 7028 cnvexg 7617 tz7.48-3 8071 errn 8301 omxpenlem 8607 sbthlem5 8620 sbthlem8 8623 sbthlem9 8624 fodomr 8657 domss2 8665 rnfi 8796 zorn2lem4 9910 rnct 9936 fpwwe2lem13 10053 trclublem 14345 relexpcnv 14384 relexpnnrn 14394 invf 17028 cicsym 17064 cnvtsr 17822 znleval 20631 ordtbas2 21729 ordtcnv 21739 ordtrest2 21742 cnconn 21960 tgqtop 22250 adj1o 29599 fcoinver 30286 fresf1o 30305 fcnvgreu 30347 dfcnv2 30351 cycpmfvlem 30682 cycpmfv1 30683 cycpmfv2 30684 cycpmfv3 30685 cycpmrn 30713 cnvordtrestixx 31056 xrge0iifhmeo 31079 mbfmcst 31417 0rrv 31609 elrn3 32896 dfrn6 35443 cnvresrn 35488 dmcoss2 35576 cnvrcl0 39865 conrel2d 39889 relexpaddss 39943 rntrclfvRP 39956 ntrneifv2 40310 |
Copyright terms: Public domain | W3C validator |