This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Define the range of a class. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } ( ex-rn ). Contrast with domain (defined in df-dm ). For alternate definitions, see dfrn2 , dfrn3 , and dfrn4 . The notation " ran " is used by Enderton. The range of a function is often also called "the image of the function" (see definition in Lang p. ix), which can be justified by imadmrn . Not to be confused with "codomain" (see df-f ), which may be a superset/superclass of the range (see frn ). (Contributed by NM, 1-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-rn | ⊢ ran 𝐴 = dom ◡ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | 0 | crn | ⊢ ran 𝐴 |
| 2 | 0 | ccnv | ⊢ ◡ 𝐴 |
| 3 | 2 | cdm | ⊢ dom ◡ 𝐴 |
| 4 | 1 3 | wceq | ⊢ ran 𝐴 = dom ◡ 𝐴 |