![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-rn | Unicode version |
Description: Define the range of a
class. For example, F = { ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-rn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | 1 | crn 4548 |
. 2
![]() ![]() ![]() |
3 | 1 | ccnv 4546 |
. . 3
![]() ![]() ![]() |
4 | 3 | cdm 4547 |
. 2
![]() ![]() ![]() ![]() |
5 | 2, 4 | wceq 1332 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfrn2 4735 dmcnvcnv 4771 rncnvcnv 4772 rneq 4774 rnss 4777 brelrng 4778 nfrn 4792 rncoss 4817 rncoeq 4820 cnvimarndm 4911 rnun 4955 rnin 4956 rnxpm 4976 rnxpss 4978 imainrect 4992 rnsnopg 5025 cnvssrndm 5068 cocnvss 5072 unidmrn 5079 dfdm2 5081 cnvexg 5084 fncnv 5197 funcnvres 5204 funimacnv 5207 fimacnvdisj 5315 dff1o4 5383 foimacnv 5393 funcocnv2 5400 f1ompt 5579 errn 6459 funrnfi 6838 sbthlemi5 6857 sbthlemi8 6860 sbthlemi9 6861 casefun 6978 caseinj 6982 djufun 6997 djuinj 6999 ctssdccl 7004 exmidfodomrlemim 7074 |
Copyright terms: Public domain | W3C validator |