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

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