Definition df-rn 5415

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 27991). Contrast with domain (defined in df-dm 5414). For alternate definitions, see dfrn2 5606, dfrn3 5607, and dfrn4 5896. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (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 5405	. 2 class ran 𝐴
3	1	ccnv 5403	. . 3 class ◡𝐴
4	3	cdm 5404	. 2 class dom ◡𝐴
5	2, 4	wceq 1507	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5606  dmcnvcnv  5643  rncnvcnv  5644  rneq  5646  rnss  5649  brelrng  5651  nfrn  5664  rncoss  5682  rncoeq  5685  cnvimarndm  5788  rnun  5842  rnin  5843  rnxp  5865  rnxpss  5867  imainrect  5876  rnsnopg  5915  cnvssrndm  5958  unidmrn  5966  dfdm2  5968  funcnvpr  6247  funcnvtp  6248  funcnvqp  6249  fncnv  6258  funcnvres  6263  funimacnv  6266  fimacnvdisj  6384  dff1o4  6450  foimacnv  6459  funcocnv2  6466  f1ompt  6696  nvof1o  6860  cnvexg  7442  tz7.48-3  7880  errn  8107  omxpenlem  8410  sbthlem5  8423  sbthlem8  8426  sbthlem9  8427  fodomr  8460  domss2  8468  rnfi  8598  zorn2lem4  9715  rnct  9741  fpwwe2lem13  9858  trclublem  14210  relexpcnv  14249  relexpnnrn  14259  invf  16890  cicsym  16926  cnvtsr  17684  znleval  20397  ordtbas2  21497  ordtcnv  21507  ordtrest2  21510  cnconn  21728  tgqtop  22018  adj1o  29446  fcoinver  30115  fresf1o  30133  fcnvgreu  30174  dfcnv2  30178  cnvordtrestixx  30791  xrge0iifhmeo  30814  mbfmcst  31153  0rrv  31346  elrn3  32488  dfrn6  34982  cnvresrn  35029  dmcoss2  35117  cnvrcl0  39326  conrel2d  39350  relexpaddss  39404  rntrclfvRP  39417  ntrneifv2  39771