df-rn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-rn		Structured version Visualization version GIF version

Definition df-rn 5693

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30373). Contrast with domain (defined in df-dm 5692). For alternate definitions, see dfrn2 5895, dfrn3 5896, and dfrn4 6213. 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 6079. Not to be confused with "codomain" (see df-f 6558), which may be a superset/superclass of the range (see frn 6735). (Contributed by NM, 1-Aug-1994.)

**Assertion**
Ref	Expression
df-rn	⊢ ran 𝐴 = dom ^◡𝐴

**Detailed syntax breakdown of Definition df-rn**
Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	crn 5683	. 2 class ran 𝐴
3	1	ccnv 5681	. . 3 class ^◡𝐴
4	3	cdm 5682	. 2 class dom ^◡𝐴
5	2, 4	wceq 1534	1 wff ran 𝐴 = dom ^◡𝐴

Colors of variables: wff setvar class

This definition is referenced by: dfrn2 5895 dmcnvcnv 5939 rncnvcnv 5940 rneq 5942 rnss 5945 brelrng 5947 nfrn 5958 rncoss 5979 rncoeq 5982 cnvimarndm 6092 rnun 6157 rnin 6158 rnxp 6181 rnxpss 6183 imainrect 6192 rnsnopg 6232 cnvssrndm 6282 unidmrn 6290 dfdm2 6292 funcnvpr 6621 funcnvtp 6622 funcnvqp 6623 fncnv 6632 funcnvres 6637 funimacnv 6640 fimacnvdisj 6780 dff1o4 6851 foimacnv 6860 funcocnv2 6868 f1ompt 7125 nvof1o 7294 cnvexg 7937 tz7.48-3 8474 errn 8756 omxpenlem 9111 sbthlem5 9125 sbthlem8 9128 sbthlem9 9129 fodomr 9166 domss2 9174 fodomfir 9370 rnfi 9382 zorn2lem4 10542 rnct 10568 fpwwe2lem12 10685 trclublem 15000 relexpcnv 15040 relexpnnrn 15050 invf 17784 cicsym 17820 cnvtsr 18613 znleval 21552 ordtbas2 23186 ordtcnv 23196 ordtrest2 23199 cnconn 23417 tgqtop 23707 adj1o 31827 fcoinver 32524 fresf1o 32548 fcnvgreu 32590 dfcnv2 32593 preiman0 32621 gsumhashmul 32925 cycpmfvlem 32990 cycpmfv1 32991 cycpmfv2 32992 cycpmfv3 32993 cycpmrn 33021 cnvordtrestixx 33728 xrge0iifhmeo 33751 mbfmcst 34093 0rrv 34285 elrn3 35584 dfrn6 38000 cnvresrn 38046 dmcoss2 38152 cnvrcl0 43292 conrel2d 43331 relexpaddss 43385 rntrclfvRP 43398 ntrneifv2 43747

W3C validator

	
		OSZAR »