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 5048 and dfrel3 5055. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 4603 | . 2 wff Rel 𝐴 |
3 | cvv 2721 | . . . 4 class V | |
4 | 3, 3 | cxp 4596 | . . 3 class (V × V) |
5 | 1, 4 | wss 3111 | . 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 4636 0nelrel 4644 releq 4680 nfrel 4683 sbcrel 4684 relss 4685 ssrel 4686 elrel 4700 relsng 4701 relsn 4703 relxp 4707 relun 4715 reliun 4719 reliin 4720 rel0 4723 relopabi 4724 relop 4748 eqbrrdva 4768 elreldm 4824 issref 4980 cnvcnv 5050 relrelss 5124 cnviinm 5139 nfunv 5215 funinsn 5231 oprabss 5919 1st2nd 6141 1stdm 6142 releldm2 6145 reldmtpos 6212 dmtpos 6215 dftpos4 6222 tpostpos 6223 iinerm 6564 fundmen 6763 frecuzrdgtcl 10337 frecuzrdgfunlem 10344 reldvg 13195 |
Copyright terms: Public domain | W3C validator |