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

Definition df-rn 5015
Description: Define the range of a class. For example, ={<.2,6>.,<.3,9>.}->ran ={6,9} (ex-rn 25161). Contrast with domain (defined in df-dm 5014). For alternate definitions, see dfrn2 5196, dfrn3 5197, and dfrn4 5472. 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 5005 . 2
31ccnv 5003 . . 3
43cdm 5004 . 2
52, 4wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfrn2  5196  dmcnvcnv  5230  rncnvcnv  5231  rneq  5233  rnss  5236  brelrng  5237  nfrn  5250  rncoss  5268  rncoeq  5271  cnvimarndm  5363  rnun  5419  rnin  5420  rnxp  5442  rnxpss  5444  imainrect  5453  rnsnopg  5492  cnvssrndm  5534  unidmrn  5542  dfdm2  5544  fncnv  5657  funcnvres  5662  funimacnv  5665  fimacnvdisj  5768  dff1o4  5829  foimacnv  5838  funcocnv2  5845  f1ompt  6053  nvof1o  6186  cnvexg  6746  tz7.48-3  7128  errn  7352  omxpenlem  7638  sbthlem5  7651  sbthlem8  7654  sbthlem9  7655  fodomr  7688  domss2  7696  rnfi  7825  zorn2lem4  8900  fpwwe2lem13  9041  invf  15162  cnvtsr  15852  znleval  18593  ordtbas2  19692  ordtcnv  19702  ordtrest2  19705  cnconn  19923  tgqtop  20213  adj1o  26813  fcoinver  27460  fcnvgreu  27514  dfcnv2  27517  rnct  27539  cnvordtrestixx  27895  xrge0iifhmeo  27918  mbfmcst  28230  0rrv  28390  elrn3  29192  cicsym  32588  conrel2d  37762  trclubg  37785
  Copyright terms: Public domain W3C validator