![]() |
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 4289 |
. 2
![]() ![]() ![]() |
3 | 1 | ccnv 4287 |
. . 3
![]() ![]() ![]() |
4 | 3 | cdm 4288 |
. 2
![]() ![]() ![]() ![]() |
5 | 2, 4 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfrn2 4466 dmcnvcnv 4501 rncnvcnv 4502 rneq 4504 rnss 4507 brelrng 4508 nfrn 4522 rncoss 4545 rncoeq 4548 cnvimarndm 4632 rnun 4675 rnin 4676 rnxpm 4695 rnxpss 4697 imainrect 4709 rnsnopg 4742 cnvssrndm 4785 unidmrn 4793 dfdm2 4795 cnvexg 4798 fncnv 4908 funcnvres 4915 funimacnv 4918 fimacnvdisj 5017 dff1o4 5077 foimacnv 5087 funcocnv2 5094 f1ompt 5263 errn 6064 |
Copyright terms: Public domain | W3C validator |