![]() |
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 5097 and dfrel3 5104. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 4649 | . 2 wff Rel 𝐴 |
3 | cvv 2752 | . . . 4 class V | |
4 | 3, 3 | cxp 4642 | . . 3 class (V × V) |
5 | 1, 4 | wss 3144 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 105 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
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 5981 1st2nd 6205 1stdm 6206 releldm2 6209 reldmtpos 6277 dmtpos 6280 dftpos4 6287 tpostpos 6288 iinerm 6632 fundmen 6831 frecuzrdgtcl 10442 frecuzrdgfunlem 10449 reldvdsrsrg 13439 reldvg 14600 |
Copyright terms: Public domain | W3C validator |