![]() |
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 6195 and dfrel3 6204. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 5683 | . 2 wff Rel 𝐴 |
3 | cvv 3461 | . . . 4 class V | |
4 | 3, 3 | cxp 5676 | . . 3 class (V × V) |
5 | 1, 4 | wss 3944 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 205 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: relxp 5696 pwvrel 5728 brrelex12 5730 0nelrel0 5738 releq 5778 nfrel 5781 sbcrel 5782 relss 5783 ssrel 5784 ssrelOLD 5785 elrel 5800 rel0 5801 nrelv 5802 relsng 5803 relun 5813 reliun 5818 reliin 5819 relopabiv 5822 relopabi 5824 relopabiALT 5825 exopxfr2 5847 relop 5853 eqbrrdva 5872 elreldm 5937 cnvcnv 6198 relrelss 6279 cnviin 6292 dff3 7109 oprabss 7527 relmptopab 7671 1st2nd 8044 1stdm 8045 releldm2 8048 relmpoopab 8099 reldmtpos 8240 dmtpos 8244 dftpos4 8251 tpostpos 8252 iiner 8808 fundmen 9056 nqerf 10955 uzrdgfni 13959 hashfun 14432 reltrclfv 15000 homarel 18028 relxpchom 18175 ustrel 24160 utop2nei 24199 utop3cls 24200 metustrel 24505 pi1xfrcnv 25028 reldv 25843 dvbsss 25875 ssrelf 32484 1stpreimas 32567 fpwrelmap 32597 gsumhashmul 32860 metideq 33625 metider 33626 pstmfval 33628 esum2d 33843 txprel 35606 relsset 35615 elfuns 35642 fnsingle 35646 funimage 35655 bj-opelrelex 36754 bj-elid5 36779 mblfinlem1 37261 rngosn3 37528 xrnrel 37975 elrelsrel 38089 dihvalrel 40882 cnvcnvintabd 43172 cnvintabd 43175 clcnvlem 43195 rfovcnvf1od 43576 relopabVD 44482 sprsymrelfo 46974 |
Copyright terms: Public domain | W3C validator |