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 6085 and dfrel3 6094. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 5589 | . 2 wff Rel 𝐴 |
3 | cvv 3429 | . . . 4 class V | |
4 | 3, 3 | cxp 5582 | . . 3 class (V × V) |
5 | 1, 4 | wss 3886 | . 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 5602 pwvrel 5632 brrelex12 5634 0nelrel0 5642 releq 5681 nfrel 5684 sbcrel 5685 relss 5686 ssrel 5687 elrel 5701 rel0 5702 nrelv 5703 relsng 5704 relun 5714 reliun 5719 reliin 5720 relopabiv 5723 relopabi 5725 relopabiALT 5726 exopxfr2 5746 relop 5752 eqbrrdva 5771 elreldm 5837 cnvcnv 6088 relrelss 6169 cnviin 6182 dff3 6968 oprabss 7371 relmptopab 7509 1st2nd 7869 1stdm 7870 releldm2 7873 relmpoopab 7921 reldmtpos 8037 dmtpos 8041 dftpos4 8048 tpostpos 8049 iiner 8565 fundmen 8808 nqerf 10696 uzrdgfni 13688 hashfun 14162 reltrclfv 14738 homarel 17761 relxpchom 17908 ustrel 23373 utop2nei 23412 utop3cls 23413 metustrel 23718 pi1xfrcnv 24230 reldv 25044 dvbsss 25076 ssrelf 30963 1stpreimas 31046 fpwrelmap 31076 gsumhashmul 31324 metideq 31851 metider 31852 pstmfval 31854 esum2d 32069 txprel 34189 relsset 34198 elfuns 34225 fnsingle 34229 funimage 34238 bj-opelrelex 35323 bj-elid5 35348 mblfinlem1 35822 rngosn3 36090 xrnrel 36511 elrelsrel 36613 dihvalrel 39301 cnvcnvintabd 41189 cnvintabd 41192 clcnvlem 41212 rfovcnvf1od 41593 relopabVD 42502 sprsymrelfo 44927 |
Copyright terms: Public domain | W3C validator |