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 26689). Contrast with domain (defined in df-dm 5048). For alternate definitions, see dfrn2 5233, dfrn3 5234, and dfrn4 5513. 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 5039 | . 2 class ran 𝐴 |
3 | 1 | ccnv 5037 | . . 3 class ◡𝐴 |
4 | 3 | cdm 5038 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1475 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff setvar class |
This definition is referenced by: dfrn2 5233 dmcnvcnv 5269 rncnvcnv 5270 rneq 5272 rnss 5275 brelrng 5276 nfrn 5289 rncoss 5307 rncoeq 5310 cnvimarndm 5405 rnun 5460 rnin 5461 rnxp 5483 rnxpss 5485 imainrect 5494 rnsnopg 5532 cnvssrndm 5574 unidmrn 5582 dfdm2 5584 funcnvpr 5864 funcnvtp 5865 funcnvqp 5866 funcnvqpOLD 5867 fncnv 5876 funcnvres 5881 funimacnv 5884 fimacnvdisj 5996 dff1o4 6058 foimacnv 6067 funcocnv2 6074 f1ompt 6290 nvof1o 6436 cnvexg 7005 tz7.48-3 7426 errn 7651 omxpenlem 7946 sbthlem5 7959 sbthlem8 7962 sbthlem9 7963 fodomr 7996 domss2 8004 rnfi 8132 zorn2lem4 9204 fpwwe2lem13 9343 trclublem 13582 relexpcnv 13623 relexpnnrn 13633 invf 16251 cicsym 16287 cnvtsr 17045 znleval 19722 ordtbas2 20805 ordtcnv 20815 ordtrest2 20818 cnconn 21035 tgqtop 21325 adj1o 28137 fcoinver 28798 fresf1o 28815 fcnvgreu 28855 dfcnv2 28859 rnct 28879 cnvordtrestixx 29287 xrge0iifhmeo 29310 mbfmcst 29648 0rrv 29840 elrn3 30906 cnvrcl0 36951 conrel2d 36975 relexpaddss 37029 rntrclfvRP 37042 ntrneifv2 37398 |
Copyright terms: Public domain | W3C validator |