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

Definition df-rn 4880
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21736). Contrast with domain (defined in df-dm 4879). For alternate definitions, see dfrn2 5050, dfrn3 5051, and dfrn4 5322. 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 4870 . 2  class  ran  A
31ccnv 4868 . . 3  class  `' A
43cdm 4869 . 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  5050  dmcnvcnv  5083  rncnvcnv  5084  rneq  5086  rnss  5089  brelrng  5090  nfrn  5103  rncoss  5127  rncoeq  5130  cnvimarndm  5216  rnun  5271  rnin  5272  rnxp  5290  rnxpss  5292  imainrect  5303  rnsnopg  5340  cnvssrndm  5382  unidmrn  5390  dfdm2  5392  cnvexg  5396  fncnv  5506  funcnvres  5513  funimacnv  5516  fimacnvdisj  5612  dff1o4  5673  foimacnv  5683  funcocnv2  5691  f1ompt  5882  tz7.48-3  6692  errn  6918  omxpenlem  7200  sbthlem5  7212  sbthlem8  7215  sbthlem9  7216  fodomr  7249  domss2  7257  rnfi  7382  zorn2lem4  8368  fpwwe2lem13  8506  invf  13981  cnvtsr  14642  znleval  16823  ordtbas2  17243  ordtcnv  17253  ordtrest2  17256  cnconn  17473  tgqtop  17732  adj1o  23385  nvof1o  24028  rnct  24096  cnvordtrestixx  24299  xrge0iifhmeo  24310  mbfmcst  24597  0rrv  24697  elrn3  25375
  Copyright terms: Public domain W3C validator