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

Definition df-rn 4848
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 21701). Contrast with domain (defined in df-dm 4847). For alternate definitions, see dfrn2 5018, dfrn3 5019, and dfrn4 5290. 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 4838 . 2  class  ran  A
31ccnv 4836 . . 3  class  `' A
43cdm 4837 . 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  5018  dmcnvcnv  5051  rncnvcnv  5052  rneq  5054  rnss  5057  brelrng  5058  nfrn  5071  rncoss  5095  rncoeq  5098  cnvimarndm  5184  rnun  5239  rnin  5240  rnxp  5258  rnxpss  5260  imainrect  5271  rnsnopg  5308  cnvssrndm  5350  unidmrn  5358  dfdm2  5360  cnvexg  5364  fncnv  5474  funcnvres  5481  funimacnv  5484  fimacnvdisj  5580  dff1o4  5641  foimacnv  5651  funcocnv2  5659  f1ompt  5850  tz7.48-3  6660  errn  6886  omxpenlem  7168  sbthlem5  7180  sbthlem8  7183  sbthlem9  7184  fodomr  7217  domss2  7225  rnfi  7350  zorn2lem4  8335  fpwwe2lem13  8473  invf  13948  cnvtsr  14609  znleval  16790  ordtbas2  17209  ordtcnv  17219  ordtrest2  17222  cnconn  17438  tgqtop  17697  adj1o  23350  nvof1o  23993  rnct  24061  cnvordtrestixx  24264  xrge0iifhmeo  24275  mbfmcst  24562  0rrv  24662  elrn3  25334
  Copyright terms: Public domain W3C validator