![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-rel | Unicode version |
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5097 and dfrel3 5104. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | 1 | wrel 4649 |
. 2
![]() ![]() ![]() |
3 | cvv 2752 |
. . . 4
![]() ![]() | |
4 | 3, 3 | cxp 4642 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | wss 3144 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: brrelex12 4682 0nelrel 4690 releq 4726 nfrel 4729 sbcrel 4730 relss 4731 ssrel 4732 elrel 4746 relsng 4747 relsn 4749 relxp 4753 relun 4761 reliun 4765 reliin 4766 rel0 4769 relopabi 4770 relop 4795 eqbrrdva 4815 elreldm 4871 issref 5029 cnvcnv 5099 relrelss 5173 cnviinm 5188 nfunv 5268 funinsn 5284 oprabss 5982 1st2nd 6206 1stdm 6207 releldm2 6210 reldmtpos 6278 dmtpos 6281 dftpos4 6288 tpostpos 6289 iinerm 6633 fundmen 6832 frecuzrdgtcl 10443 frecuzrdgfunlem 10450 relelbasov 12574 reldvdsrsrg 13442 reldvg 14605 |
Copyright terms: Public domain | W3C validator |