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

Definition df-rn 4822
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21589). Contrast with domain (defined in df-dm 4821). For alternate definitions, see dfrn2 4992, dfrn3 4993, and dfrn4 5264. 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 4812 . 2  class  ran  A
31ccnv 4810 . . 3  class  `' A
43cdm 4811 . 2  class  dom  `' A
52, 4wceq 1649 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4992  dmcnvcnv  5025  rncnvcnv  5026  rneq  5028  rnss  5031  brelrng  5032  nfrn  5045  rncoss  5069  rncoeq  5072  cnvimarndm  5158  rnun  5213  rnin  5214  rnxp  5232  rnxpss  5234  imainrect  5245  rnsnopg  5282  cnvssrndm  5324  unidmrn  5332  dfdm2  5334  cnvexg  5338  fncnv  5448  funcnvres  5455  funimacnv  5458  fimacnvdisj  5554  dff1o4  5615  foimacnv  5625  funcocnv2  5633  f1ompt  5823  tz7.48-3  6630  errn  6856  omxpenlem  7138  sbthlem5  7150  sbthlem8  7153  sbthlem9  7154  fodomr  7187  domss2  7195  rnfi  7320  zorn2lem4  8305  fpwwe2lem13  8443  invf  13913  cnvtsr  14574  znleval  16751  ordtbas2  17170  ordtcnv  17180  ordtrest2  17183  cnconn  17399  tgqtop  17658  adj1o  23238  nvof1o  23876  rnct  23942  cnvordtrestixx  24108  xrge0iifhmeo  24119  mbfmcst  24396  0rrv  24481  elrn3  25137
  Copyright terms: Public domain W3C validator