![]() |
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 27991). Contrast with domain (defined in df-dm 5414). For alternate definitions, see dfrn2 5606, dfrn3 5607, and dfrn4 5896. 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 5405 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5403 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5404 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1507 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5606 dmcnvcnv 5643 rncnvcnv 5644 rneq 5646 rnss 5649 brelrng 5651 nfrn 5664 rncoss 5682 rncoeq 5685 cnvimarndm 5788 rnun 5842 rnin 5843 rnxp 5865 rnxpss 5867 imainrect 5876 rnsnopg 5915 cnvssrndm 5958 unidmrn 5966 dfdm2 5968 funcnvpr 6247 funcnvtp 6248 funcnvqp 6249 fncnv 6258 funcnvres 6263 funimacnv 6266 fimacnvdisj 6384 dff1o4 6450 foimacnv 6459 funcocnv2 6466 f1ompt 6696 nvof1o 6860 cnvexg 7442 tz7.48-3 7880 errn 8107 omxpenlem 8410 sbthlem5 8423 sbthlem8 8426 sbthlem9 8427 fodomr 8460 domss2 8468 rnfi 8598 zorn2lem4 9715 rnct 9741 fpwwe2lem13 9858 trclublem 14210 relexpcnv 14249 relexpnnrn 14259 invf 16890 cicsym 16926 cnvtsr 17684 znleval 20397 ordtbas2 21497 ordtcnv 21507 ordtrest2 21510 cnconn 21728 tgqtop 22018 adj1o 29446 fcoinver 30115 fresf1o 30133 fcnvgreu 30174 dfcnv2 30178 cnvordtrestixx 30791 xrge0iifhmeo 30814 mbfmcst 31153 0rrv 31346 elrn3 32488 dfrn6 34982 cnvresrn 35029 dmcoss2 35117 cnvrcl0 39326 conrel2d 39350 relexpaddss 39404 rntrclfvRP 39417 ntrneifv2 39771 |
Copyright terms: Public domain | W3C validator |