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

Definition df-rn 4930
Description: Define the range of a class. For example, ?Error: 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } ^ This math symbol is not active (i.e. was not declared in this scope). ={<.2,6>.,<.3,9>.}->ran ={6,9} (ex-rn 21799). Contrast with domain (defined in df-dm 4929). For alternate definitions, see dfrn2 5103, dfrn3 5104, and dfrn4 5375. 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

Detailed syntax breakdown of Definition df-rn
StepHypRef Expression
1 cA . . 3
21crn 4920 . 2
31ccnv 4918 . . 3
43cdm 4919 . 2
52, 4wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  dfrn2  5103  dmcnvcnv  5136  rncnvcnv  5137  rneq  5139  rnss  5142  brelrng  5143  nfrn  5156  rncoss  5179  rncoeq  5182  cnvimarndm  5269  rnun  5324  rnin  5325  rnxp  5343  rnxpss  5345  imainrect  5356  rnsnopg  5395  cnvssrndm  5437  unidmrn  5445  dfdm2  5447  cnvexg  5451  fncnv  5562  funcnvres  5569  funimacnv  5572  fimacnvdisj  5668  dff1o4  5729  foimacnv  5739  funcocnv2  5747  f1ompt  5939  tz7.48-3  6750  errn  6976  omxpenlem  7258  sbthlem5  7270  sbthlem8  7273  sbthlem9  7274  fodomr  7307  domss2  7315  rnfi  7440  zorn2lem4  8430  fpwwe2lem13  8568  invf  14044  cnvtsr  14705  znleval  16886  ordtbas2  17306  ordtcnv  17316  ordtrest2  17319  cnconn  17536  tgqtop  17795  adj1o  23448  nvof1o  24088  rnct  24156  cnvordtrestixx  24360  xrge0iifhmeo  24371  mbfmcst  24658  0rrv  24813  elrn3  25490
  Copyright terms: Public domain W3C validator