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

Definition df-rn 4892
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21753). Contrast with domain (defined in df-dm 4891). For alternate definitions, see dfrn2 5062, dfrn3 5063, and dfrn4 5334. 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 4882 . 2  class  ran  A
31ccnv 4880 . . 3  class  `' A
43cdm 4881 . 2  class  dom  `' A
52, 4wceq 1653 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  5062  dmcnvcnv  5095  rncnvcnv  5096  rneq  5098  rnss  5101  brelrng  5102  nfrn  5115  rncoss  5139  rncoeq  5142  cnvimarndm  5228  rnun  5283  rnin  5284  rnxp  5302  rnxpss  5304  imainrect  5315  rnsnopg  5352  cnvssrndm  5394  unidmrn  5402  dfdm2  5404  cnvexg  5408  fncnv  5518  funcnvres  5525  funimacnv  5528  fimacnvdisj  5624  dff1o4  5685  foimacnv  5695  funcocnv2  5703  f1ompt  5894  tz7.48-3  6704  errn  6930  omxpenlem  7212  sbthlem5  7224  sbthlem8  7227  sbthlem9  7228  fodomr  7261  domss2  7269  rnfi  7394  zorn2lem4  8384  fpwwe2lem13  8522  invf  13998  cnvtsr  14659  znleval  16840  ordtbas2  17260  ordtcnv  17270  ordtrest2  17273  cnconn  17490  tgqtop  17749  adj1o  23402  nvof1o  24045  rnct  24113  cnvordtrestixx  24316  xrge0iifhmeo  24327  mbfmcst  24614  0rrv  24714  elrn3  25391
  Copyright terms: Public domain W3C validator