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

Definition df-rn 4666
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 20756). Contrast with domain (defined in df-dm 4665). For alternate definitions, see dfrn2 4842, dfrn3 4843, and dfrn4 5107. 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 4648 . 2  class  ran  A
31ccnv 4646 . . 3  class  `' A
43cdm 4647 . 2  class  dom  `'  A
52, 4wceq 1619 1  wff  ran  A  =  dom  `'  A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4842  dmcnvcnv  4875  rncnvcnv  4876  rneq  4878  rnss  4881  brelrng  4882  nfrn  4895  rncoss  4919  rncoeq  4922  cnvimarndm  5008  rnun  5063  rnin  5064  rnxp  5080  rnxpss  5082  imainrect  5093  rnsnopg  5125  cnvssrndm  5167  unidmrn  5175  dfdm2  5177  cnvexg  5181  fncnv  5238  funcnvres  5245  funimacnv  5248  fimacnvdisj  5343  dff1o4  5404  foimacnv  5414  funcocnv2  5422  f1ompt  5602  tz7.48-3  6410  errn  6636  omxpenlem  6917  sbthlem5  6929  sbthlem8  6932  sbthlem9  6933  fodomr  6966  domss2  6974  rnfi  7095  zorn2lem4  8080  fpwwe2lem13  8218  invf  13618  cnvtsr  14279  znleval  16456  ordtbas2  16869  ordtcnv  16879  ordtrest2  16882  cnconn  17096  tgqtop  17351  adj1o  22420  nvof1o  22983  fldcnv  24408  rnintintrn  24479  domcnvpre  24586  ranncnt  24636  toplat  24643
  Copyright terms: Public domain W3C validator