![]() |
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 4801 and dfrel3 4808. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 4376 | . 2 wff Rel 𝐴 |
3 | cvv 2602 | . . . 4 class V | |
4 | 3, 3 | cxp 4369 | . . 3 class (V × V) |
5 | 1, 4 | wss 2974 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 103 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff set class |
This definition is referenced by: brrelex12 4407 releq 4448 nfrel 4451 sbcrel 4452 relss 4453 ssrel 4454 elrel 4468 relsng 4469 relsn 4471 relxp 4475 relun 4482 reliun 4486 reliin 4487 rel0 4490 relopabi 4491 relop 4514 eqbrrdva 4533 elreldm 4588 issref 4737 cnvcnv 4803 relrelss 4874 cnviinm 4889 nfunv 4963 funinsn 4979 oprabss 5621 1st2nd 5838 1stdm 5839 releldm2 5842 reldmtpos 5902 dmtpos 5905 dftpos4 5912 tpostpos 5913 iinerm 6244 fundmen 6353 frecuzrdgtcl 9494 frecuzrdgfunlem 9501 |
Copyright terms: Public domain | W3C validator |