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

Definition df-rn 4889
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21748). Contrast with domain (defined in df-dm 4888). For alternate definitions, see dfrn2 5059, dfrn3 5060, and dfrn4 5331. 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 4879 . 2  class  ran  A
31ccnv 4877 . . 3  class  `' A
43cdm 4878 . 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  5059  dmcnvcnv  5092  rncnvcnv  5093  rneq  5095  rnss  5098  brelrng  5099  nfrn  5112  rncoss  5136  rncoeq  5139  cnvimarndm  5225  rnun  5280  rnin  5281  rnxp  5299  rnxpss  5301  imainrect  5312  rnsnopg  5349  cnvssrndm  5391  unidmrn  5399  dfdm2  5401  cnvexg  5405  fncnv  5515  funcnvres  5522  funimacnv  5525  fimacnvdisj  5621  dff1o4  5682  foimacnv  5692  funcocnv2  5700  f1ompt  5891  tz7.48-3  6701  errn  6927  omxpenlem  7209  sbthlem5  7221  sbthlem8  7224  sbthlem9  7225  fodomr  7258  domss2  7266  rnfi  7391  zorn2lem4  8379  fpwwe2lem13  8517  invf  13993  cnvtsr  14654  znleval  16835  ordtbas2  17255  ordtcnv  17265  ordtrest2  17268  cnconn  17485  tgqtop  17744  adj1o  23397  nvof1o  24040  rnct  24108  cnvordtrestixx  24311  xrge0iifhmeo  24322  mbfmcst  24609  0rrv  24709  elrn3  25386
  Copyright terms: Public domain W3C validator