Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-rel | GIF version |
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5061 and dfrel3 5068. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 4616 | . 2 wff Rel 𝐴 |
3 | cvv 2730 | . . . 4 class V | |
4 | 3, 3 | cxp 4609 | . . 3 class (V × V) |
5 | 1, 4 | wss 3121 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 104 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff set class |
This definition is referenced by: brrelex12 4649 0nelrel 4657 releq 4693 nfrel 4696 sbcrel 4697 relss 4698 ssrel 4699 elrel 4713 relsng 4714 relsn 4716 relxp 4720 relun 4728 reliun 4732 reliin 4733 rel0 4736 relopabi 4737 relop 4761 eqbrrdva 4781 elreldm 4837 issref 4993 cnvcnv 5063 relrelss 5137 cnviinm 5152 nfunv 5231 funinsn 5247 oprabss 5939 1st2nd 6160 1stdm 6161 releldm2 6164 reldmtpos 6232 dmtpos 6235 dftpos4 6242 tpostpos 6243 iinerm 6585 fundmen 6784 frecuzrdgtcl 10368 frecuzrdgfunlem 10375 reldvg 13442 |
Copyright terms: Public domain | W3C validator |