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

Definition df-rn 4700
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 20827). Contrast with domain (defined in df-dm 4699). For alternate definitions, see dfrn2 4868, dfrn3 4869, and dfrn4 5134. 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 4690 . 2  class  ran  A
31ccnv 4688 . . 3  class  `' A
43cdm 4689 . 2  class  dom  `' A
52, 4wceq 1623 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4868  dmcnvcnv  4901  rncnvcnv  4902  rneq  4904  rnss  4907  brelrng  4908  nfrn  4921  rncoss  4945  rncoeq  4948  cnvimarndm  5034  rnun  5089  rnin  5090  rnxp  5106  rnxpss  5108  imainrect  5119  rnsnopg  5152  cnvssrndm  5194  unidmrn  5202  dfdm2  5204  cnvexg  5208  fncnv  5314  funcnvres  5321  funimacnv  5324  fimacnvdisj  5419  dff1o4  5480  foimacnv  5490  funcocnv2  5498  f1ompt  5682  tz7.48-3  6456  errn  6682  omxpenlem  6963  sbthlem5  6975  sbthlem8  6978  sbthlem9  6979  fodomr  7012  domss2  7020  rnfi  7141  zorn2lem4  8126  fpwwe2lem13  8264  invf  13670  cnvtsr  14331  znleval  16508  ordtbas2  16921  ordtcnv  16931  ordtrest2  16934  cnconn  17148  tgqtop  17403  adj1o  22474  nvof1o  23036  cnvordtrestixx  23297  xrge0iifhmeo  23318  rnct  23344  mbfmcst  23564  0rrv  23654  elrn3  24120  fldcnv  25056  rnintintrn  25126  domcnvpre  25233  ranncnt  25283  toplat  25290
  Copyright terms: Public domain W3C validator