Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-rel | Structured version Visualization version GIF version |
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6040 and dfrel3 6049. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 5554 | . 2 wff Rel 𝐴 |
3 | cvv 3495 | . . . 4 class V | |
4 | 3, 3 | cxp 5547 | . . 3 class (V × V) |
5 | 1, 4 | wss 3935 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 207 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: relxp 5567 pwvrel 5596 brrelex12 5598 0nelrel0 5606 releq 5645 nfrel 5648 sbcrel 5649 relss 5650 ssrel 5651 elrel 5665 rel0 5666 nrelv 5667 relsng 5668 relun 5678 reliun 5683 reliin 5684 relopabiv 5687 relopabi 5688 relopabiALT 5689 exopxfr2 5709 relop 5715 eqbrrdva 5734 elreldm 5799 cnvcnv 6043 relrelss 6118 cnviin 6131 dff3 6859 oprabss 7249 relmptopab 7384 1st2nd 7729 1stdm 7730 releldm2 7733 relmpoopab 7780 reldmtpos 7891 dmtpos 7895 dftpos4 7902 tpostpos 7903 iiner 8359 fundmen 8572 nqerf 10341 uzrdgfni 13316 hashfun 13788 reltrclfv 14367 homarel 17286 relxpchom 17421 ustrel 22749 utop2nei 22788 utop3cls 22789 metustrel 23091 pi1xfrcnv 23590 reldv 24397 dvbsss 24429 ssrelf 30295 1stpreimas 30368 fpwrelmap 30396 metideq 31033 metider 31034 pstmfval 31036 esum2d 31252 txprel 33238 relsset 33247 elfuns 33274 fnsingle 33278 funimage 33287 bj-opelrelex 34329 bj-elid5 34354 mblfinlem1 34811 rngosn3 35085 xrnrel 35507 elrelsrel 35609 dihvalrel 38297 cnvcnvintabd 39840 cnvintabd 39843 clcnvlem 39863 rfovcnvf1od 40230 relopabVD 41115 sprsymrelfo 43506 |
Copyright terms: Public domain | W3C validator |