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

Definition df-rn 4881
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21740). Contrast with domain (defined in df-dm 4880). For alternate definitions, see dfrn2 5051, dfrn3 5052, and dfrn4 5323. 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 4871 . 2  class  ran  A
31ccnv 4869 . . 3  class  `' A
43cdm 4870 . 2  class  dom  `' A
52, 4wceq 1652 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  5051  dmcnvcnv  5084  rncnvcnv  5085  rneq  5087  rnss  5090  brelrng  5091  nfrn  5104  rncoss  5128  rncoeq  5131  cnvimarndm  5217  rnun  5272  rnin  5273  rnxp  5291  rnxpss  5293  imainrect  5304  rnsnopg  5341  cnvssrndm  5383  unidmrn  5391  dfdm2  5393  cnvexg  5397  fncnv  5507  funcnvres  5514  funimacnv  5517  fimacnvdisj  5613  dff1o4  5674  foimacnv  5684  funcocnv2  5692  f1ompt  5883  tz7.48-3  6693  errn  6919  omxpenlem  7201  sbthlem5  7213  sbthlem8  7216  sbthlem9  7217  fodomr  7250  domss2  7258  rnfi  7383  zorn2lem4  8371  fpwwe2lem13  8509  invf  13985  cnvtsr  14646  znleval  16827  ordtbas2  17247  ordtcnv  17257  ordtrest2  17260  cnconn  17477  tgqtop  17736  adj1o  23389  nvof1o  24032  rnct  24100  cnvordtrestixx  24303  xrge0iifhmeo  24314  mbfmcst  24601  0rrv  24701  elrn3  25378
  Copyright terms: Public domain W3C validator