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

Definition df-rn 4873
Description: Define the range of a class. For example, ={<.2,6>.,<.3,9>.}->ran ={6,9} (ex-rn 22769). Contrast with domain (defined in df-dm 4872). For alternate definitions, see dfrn2 5050, dfrn3 5051, and dfrn4 5318. 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 4863 . 2
31ccnv 4861 . . 3
43cdm 4862 . 2
52, 4wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  dfrn2  5050  dmcnvcnv  5084  rncnvcnv  5085  rneq  5087  rnss  5090  brelrng  5091  nfrn  5104  rncoss  5122  rncoeq  5125  cnvimarndm  5213  rnun  5267  rnin  5268  rnxp  5289  rnxpss  5291  imainrect  5300  rnsnopg  5338  cnvssrndm  5379  unidmrn  5387  dfdm2  5389  fncnv  5500  funcnvres  5505  funimacnv  5508  fimacnvdisj  5606  dff1o4  5666  foimacnv  5675  funcocnv2  5682  f1ompt  5881  cnvexg  6532  tz7.48-3  6863  errn  7089  omxpenlem  7374  sbthlem5  7386  sbthlem8  7389  sbthlem9  7390  fodomr  7423  domss2  7431  rnfi  7557  zorn2lem4  8550  fpwwe2lem13  8688  invf  14547  cnvtsr  15233  znleval  17460  ordtbas2  18269  ordtcnv  18279  ordtrest2  18282  cnconn  18500  tgqtop  18759  adj1o  24420  nvof1o  25076  fcnvgreu  25121  dfcnv2  25124  rnct  25146  cnvordtrestixx  25522  xrge0iifhmeo  25545  mbfmcst  25854  0rrv  25984  elrn3  26725
  Copyright terms: Public domain W3C validator