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

Definition df-rn 4716
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 20843). Contrast with domain (defined in df-dm 4715). For alternate definitions, see dfrn2 4884, dfrn3 4885, and dfrn4 5150. 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  A  =  dom  `' A

Detailed syntax breakdown of Definition df-rn
StepHypRef Expression
1 cA . . 3  class  A
21crn 4706 . 2  class  ran  A
31ccnv 4704 . . 3  class  `' A
43cdm 4705 . 2  class  dom  `' A
52, 4wceq 1632 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4884  dmcnvcnv  4917  rncnvcnv  4918  rneq  4920  rnss  4923  brelrng  4924  nfrn  4937  rncoss  4961  rncoeq  4964  cnvimarndm  5050  rnun  5105  rnin  5106  rnxp  5122  rnxpss  5124  imainrect  5135  rnsnopg  5168  cnvssrndm  5210  unidmrn  5218  dfdm2  5220  cnvexg  5224  fncnv  5330  funcnvres  5337  funimacnv  5340  fimacnvdisj  5435  dff1o4  5496  foimacnv  5506  funcocnv2  5514  f1ompt  5698  tz7.48-3  6472  errn  6698  omxpenlem  6979  sbthlem5  6991  sbthlem8  6994  sbthlem9  6995  fodomr  7028  domss2  7036  rnfi  7157  zorn2lem4  8142  fpwwe2lem13  8280  invf  13686  cnvtsr  14347  znleval  16524  ordtbas2  16937  ordtcnv  16947  ordtrest2  16950  cnconn  17164  tgqtop  17419  adj1o  22490  nvof1o  23052  cnvordtrestixx  23312  xrge0iifhmeo  23333  rnct  23359  mbfmcst  23579  0rrv  23669  elrn3  24191  fldcnv  25159  rnintintrn  25229  domcnvpre  25336  ranncnt  25386  toplat  25393
  Copyright terms: Public domain W3C validator