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 5502 and dfrel3 5510. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rel | ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wrel 5043 | . 2 wff Rel 𝐴 |
3 | cvv 3173 | . . . 4 class V | |
4 | 3, 3 | cxp 5036 | . . 3 class (V × V) |
5 | 1, 4 | wss 3540 | . 2 wff 𝐴 ⊆ (V × V) |
6 | 2, 5 | wb 195 | 1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: brrelex12 5079 releq 5124 nfrel 5127 sbcrel 5128 relss 5129 ssrel 5130 ssrelOLD 5131 elrel 5145 relsn 5146 relxp 5150 relun 5158 reliun 5162 reliin 5163 rel0 5166 relopabi 5167 relopabiALT 5168 exopxfr2 5188 relop 5194 eqbrrdva 5213 elreldm 5271 issref 5428 cnvcnv 5505 relrelss 5576 cnviin 5589 nfunv 5835 dff3 6280 oprabss 6644 relmptopab 6781 1st2nd 7105 1stdm 7106 releldm2 7109 relmpt2opab 7146 reldmtpos 7247 dmtpos 7251 dftpos4 7258 tpostpos 7259 iiner 7706 fundmen 7916 nqerf 9631 uzrdgfni 12619 hashfun 13084 reltrclfv 13606 homarel 16509 relxpchom 16644 ustrel 21825 utop2nei 21864 utop3cls 21865 metustrel 22167 pi1xfrcnv 22665 reldv 23440 dvbsss 23472 uhgraopelvv 25826 vcex 26817 ssrelf 28805 1stpreimas 28866 fpwrelmap 28896 metideq 29264 metider 29265 pstmfval 29267 esum2d 29482 txprel 31156 relsset 31165 elfuns 31192 fnsingle 31196 funimage 31205 bj-elid 32262 mblfinlem1 32616 rngosn3 32893 dihvalrel 35586 relintabex 36906 cnvcnvintabd 36925 cnvintabd 36928 clcnvlem 36949 rfovcnvf1od 37318 relopabVD 38159 |
Copyright terms: Public domain | W3C validator |