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 4959 and dfrel3 4966. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | wrel 4514 | . 2 |
3 | cvv 2660 | . . . 4 | |
4 | 3, 3 | cxp 4507 | . . 3 |
5 | 1, 4 | wss 3041 | . 2 |
6 | 2, 5 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: brrelex12 4547 0nelrel 4555 releq 4591 nfrel 4594 sbcrel 4595 relss 4596 ssrel 4597 elrel 4611 relsng 4612 relsn 4614 relxp 4618 relun 4626 reliun 4630 reliin 4631 rel0 4634 relopabi 4635 relop 4659 eqbrrdva 4679 elreldm 4735 issref 4891 cnvcnv 4961 relrelss 5035 cnviinm 5050 nfunv 5126 funinsn 5142 oprabss 5825 1st2nd 6047 1stdm 6048 releldm2 6051 reldmtpos 6118 dmtpos 6121 dftpos4 6128 tpostpos 6129 iinerm 6469 fundmen 6668 frecuzrdgtcl 10140 frecuzrdgfunlem 10147 reldvg 12728 |
Copyright terms: Public domain | W3C validator |