![]() |
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 5884 and dfrel3 5892. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 5409 | . 2 wff Rel 𝐴 |
3 | cvv 3412 | . . . 4 class V | |
4 | 3, 3 | cxp 5402 | . . 3 class (V × V) |
5 | 1, 4 | wss 3828 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 198 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: relxp 5422 brrelex12 5451 0nelrel0 5459 releq 5498 nfrel 5501 sbcrel 5502 relss 5503 ssrel 5504 elrel 5518 rel0 5519 nrelv 5520 relsng 5521 relun 5531 reliun 5536 reliin 5537 relopabiv 5540 relopabi 5541 relopabiALT 5542 exopxfr2 5562 relop 5568 eqbrrdva 5587 elreldm 5645 cnvcnv 5887 relrelss 5960 cnviin 5973 dff3 6687 oprabss 7074 relmptopab 7211 1st2nd 7547 1stdm 7548 releldm2 7551 relmpoopab 7594 reldmtpos 7700 dmtpos 7704 dftpos4 7711 tpostpos 7712 iiner 8165 fundmen 8376 nqerf 10146 uzrdgfni 13138 hashfun 13605 reltrclfv 14232 homarel 17148 relxpchom 17283 ustrel 22517 utop2nei 22556 utop3cls 22557 metustrel 22859 pi1xfrcnv 23358 reldv 24165 dvbsss 24197 ssrelf 30124 1stpreimas 30187 fpwrelmap 30215 metideq 30768 metider 30769 pstmfval 30771 esum2d 30987 txprel 32831 relsset 32840 elfuns 32867 fnsingle 32871 funimage 32880 bj-elid 33903 mblfinlem1 34348 rngosn3 34622 xrnrel 35048 elrelsrel 35150 dihvalrel 37838 relintabex 39281 cnvcnvintabd 39300 cnvintabd 39303 clcnvlem 39324 rfovcnvf1od 39691 relopabVD 40631 sprsymrelfo 43001 |
Copyright terms: Public domain | W3C validator |