![]() |
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 4925 and dfrel3 4932. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | 1 | wrel 4482 |
. 2
![]() ![]() ![]() |
3 | cvv 2641 |
. . . 4
![]() ![]() | |
4 | 3, 3 | cxp 4475 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | wss 3021 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: brrelex12 4515 0nelrel 4523 releq 4559 nfrel 4562 sbcrel 4563 relss 4564 ssrel 4565 elrel 4579 relsng 4580 relsn 4582 relxp 4586 relun 4594 reliun 4598 reliin 4599 rel0 4602 relopabi 4603 relop 4627 eqbrrdva 4647 elreldm 4703 issref 4857 cnvcnv 4927 relrelss 5001 cnviinm 5016 nfunv 5092 funinsn 5108 oprabss 5789 1st2nd 6009 1stdm 6010 releldm2 6013 reldmtpos 6080 dmtpos 6083 dftpos4 6090 tpostpos 6091 iinerm 6431 fundmen 6630 frecuzrdgtcl 10026 frecuzrdgfunlem 10033 reldvg 12521 |
Copyright terms: Public domain | W3C validator |