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 5553
Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 28228). Contrast with domain (defined in df-dm 5552). For alternate definitions, see dfrn2 5746, dfrn3 5747, and dfrn4 6046. 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 5926. Not to be confused with "codomain" (see df-f 6347), which may be a superset/superclass of the range (see frn 6509). (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 5543 . 2 class ran 𝐴
31ccnv 5541 . . 3 class 𝐴
43cdm 5542 . 2 class dom 𝐴
52, 4wceq 1538 1 wff ran 𝐴 = dom 𝐴
Colors of variables: wff setvar class
This definition is referenced by:  dfrn2  5746  dmcnvcnv  5790  rncnvcnv  5791  rneq  5793  rnss  5796  brelrng  5798  nfrn  5811  rncoss  5830  rncoeq  5833  cnvimarndm  5937  rnun  5991  rnin  5992  rnxp  6014  rnxpss  6016  imainrect  6025  rnsnopg  6065  cnvssrndm  6109  unidmrn  6117  dfdm2  6119  funcnvpr  6404  funcnvtp  6405  funcnvqp  6406  fncnv  6415  funcnvres  6420  funimacnv  6423  fimacnvdisj  6547  dff1o4  6614  foimacnv  6623  funcocnv2  6630  f1ompt  6866  nvof1o  7029  cnvexg  7624  tz7.48-3  8076  errn  8307  omxpenlem  8614  sbthlem5  8628  sbthlem8  8631  sbthlem9  8632  fodomr  8665  domss2  8673  rnfi  8804  zorn2lem4  9919  rnct  9945  fpwwe2lem13  10062  trclublem  14355  relexpcnv  14394  relexpnnrn  14404  invf  17038  cicsym  17074  cnvtsr  17832  znleval  20701  ordtbas2  21799  ordtcnv  21809  ordtrest2  21812  cnconn  22030  tgqtop  22320  adj1o  29680  fcoinver  30368  fresf1o  30387  fcnvgreu  30429  dfcnv2  30433  cycpmfvlem  30786  cycpmfv1  30787  cycpmfv2  30788  cycpmfv3  30789  cycpmrn  30817  cnvordtrestixx  31213  xrge0iifhmeo  31236  mbfmcst  31574  0rrv  31766  elrn3  33055  dfrn6  35665  cnvresrn  35710  dmcoss2  35799  cnvrcl0  40241  conrel2d  40281  relexpaddss  40335  rntrclfvRP  40348  ntrneifv2  40702
  Copyright terms: Public domain W3C validator