![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-rn | Structured version Visualization version GIF version |
Description: Define the range of a class. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → ran 𝐹 = {6, 9} (ex-rn 27427). Contrast with domain (defined in df-dm 5153). For alternate definitions, see dfrn2 5343, dfrn3 5344, and dfrn4 5630. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | crn 5144 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5142 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5143 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1523 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5343 dmcnvcnv 5380 rncnvcnv 5381 rneq 5383 rnss 5386 brelrng 5387 nfrn 5400 rncoss 5418 rncoeq 5421 cnvimarndm 5521 rnun 5576 rnin 5577 rnxp 5599 rnxpss 5601 imainrect 5610 rnsnopg 5650 cnvssrndm 5695 unidmrn 5703 dfdm2 5705 funcnvpr 5988 funcnvtp 5989 funcnvqp 5990 funcnvqpOLD 5991 fncnv 6000 funcnvres 6005 funimacnv 6008 fimacnvdisj 6121 dff1o4 6183 foimacnv 6192 funcocnv2 6199 f1ompt 6422 nvof1o 6576 cnvexg 7154 tz7.48-3 7584 errn 7809 omxpenlem 8102 sbthlem5 8115 sbthlem8 8118 sbthlem9 8119 fodomr 8152 domss2 8160 rnfi 8290 zorn2lem4 9359 rnct 9385 fpwwe2lem13 9502 trclublem 13780 relexpcnv 13819 relexpnnrn 13829 invf 16475 cicsym 16511 cnvtsr 17269 znleval 19951 ordtbas2 21043 ordtcnv 21053 ordtrest2 21056 cnconn 21273 tgqtop 21563 adj1o 28881 fcoinver 29544 fresf1o 29561 fcnvgreu 29600 dfcnv2 29604 cnvordtrestixx 30087 xrge0iifhmeo 30110 mbfmcst 30449 0rrv 30641 elrn3 31778 dfrn6 34213 cnvresrn 34256 dmcoss2 34344 cnvrcl0 38249 conrel2d 38273 relexpaddss 38327 rntrclfvRP 38340 ntrneifv2 38695 |
Copyright terms: Public domain | W3C validator |