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

Definition df-rn 5577
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.)
Assertion
Ref Expression
df-rn ran 𝐴 = dom 𝐴

Detailed syntax breakdown of Definition df-rn
StepHypRef Expression
1 cA . . 3 class 𝐴
21crn 5567 . 2 class ran 𝐴
31ccnv 5565 . . 3 class 𝐴
43cdm 5566 . 2 class dom 𝐴
52, 4wceq 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