![]() |
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 27600). Contrast with domain (defined in df-dm 5268). For alternate definitions, see dfrn2 5458, dfrn3 5459, and dfrn4 5745. 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 5259 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5257 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5258 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1624 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5458 dmcnvcnv 5495 rncnvcnv 5496 rneq 5498 rnss 5501 brelrng 5502 nfrn 5515 rncoss 5533 rncoeq 5536 cnvimarndm 5636 rnun 5691 rnin 5692 rnxp 5714 rnxpss 5716 imainrect 5725 rnsnopg 5765 cnvssrndm 5810 unidmrn 5818 dfdm2 5820 funcnvpr 6103 funcnvtp 6104 funcnvqp 6105 funcnvqpOLD 6106 fncnv 6115 funcnvres 6120 funimacnv 6123 fimacnvdisj 6236 dff1o4 6298 foimacnv 6307 funcocnv2 6314 f1ompt 6537 nvof1o 6691 cnvexg 7269 tz7.48-3 7700 errn 7925 omxpenlem 8218 sbthlem5 8231 sbthlem8 8234 sbthlem9 8235 fodomr 8268 domss2 8276 rnfi 8406 zorn2lem4 9505 rnct 9531 fpwwe2lem13 9648 trclublem 13927 relexpcnv 13966 relexpnnrn 13976 invf 16621 cicsym 16657 cnvtsr 17415 znleval 20097 ordtbas2 21189 ordtcnv 21199 ordtrest2 21202 cnconn 21419 tgqtop 21709 adj1o 29054 fcoinver 29717 fresf1o 29734 fcnvgreu 29773 dfcnv2 29777 cnvordtrestixx 30260 xrge0iifhmeo 30283 mbfmcst 30622 0rrv 30814 elrn3 31951 dfrn6 34388 cnvresrn 34431 dmcoss2 34519 cnvrcl0 38426 conrel2d 38450 relexpaddss 38504 rntrclfvRP 38517 ntrneifv2 38872 |
Copyright terms: Public domain | W3C validator |