![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relxp | Structured version Visualization version GIF version |
Description: A Cartesian product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
relxp | ⊢ Rel (𝐴 × 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpss 5265 | . 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V) | |
2 | df-rel 5256 | . 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V)) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ Rel (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3349 ⊆ wss 3721 × cxp 5247 Rel wrel 5254 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-v 3351 df-in 3728 df-ss 3735 df-opab 4845 df-xp 5255 df-rel 5256 |
This theorem is referenced by: xpsspw 5372 xpiindi 5396 eliunxp 5398 opeliunxp2 5399 relres 5567 restidsing 5599 restidsingOLD 5600 codir 5657 qfto 5658 difxp 5699 sofld 5722 cnvcnv 5727 cnvcnvOLD 5728 dfco2 5778 unixp 5812 ressn 5815 fliftcnv 6703 fliftfun 6704 oprssdm 6961 frxp 7437 opeliunxp2f 7487 reltpos 7508 tpostpos 7523 tposfo 7530 tposf 7531 swoer 7925 xpider 7969 erinxp 7972 xpcomf1o 8204 cda1dif 9199 brdom3 9551 brdom5 9552 brdom4 9553 fpwwe2lem8 9660 fpwwe2lem9 9661 fpwwe2lem12 9664 ordpinq 9966 addassnq 9981 mulassnq 9982 distrnq 9984 mulidnq 9986 recmulnq 9987 ltexnq 9998 prcdnq 10016 ltrel 10301 lerel 10303 dfle2 12184 fsumcom2 14712 fprodcom2 14920 0rest 16297 firest 16300 pwsle 16359 2oppchomf 16590 isinv 16626 invsym2 16629 invfun 16630 oppcsect2 16645 oppcinv 16646 oppchofcl 17107 oyoncl 17117 clatl 17323 gicer 17925 gsum2d2lem 18578 gsum2d2 18579 gsumcom2 18580 gsumxp 18581 dprd2d2 18650 opsrtoslem2 19699 mattpostpos 20477 mdetunilem9 20643 restbas 21182 txuni2 21588 txcls 21627 txdis1cn 21658 txkgen 21675 hmpher 21807 cnextrel 22086 tgphaus 22139 qustgplem 22143 tsmsxp 22177 utop2nei 22273 utop3cls 22274 xmeter 22457 caubl 23324 ovoliunlem1 23489 reldv 23853 taylf 24334 lgsquadlem1 25325 lgsquadlem2 25326 nvrel 27791 dfcnv2 29810 qtophaus 30237 cvmliftlem1 31599 cvmlift2lem12 31628 dfso2 31976 elrn3 31984 relbigcup 32335 poimirlem3 33738 heicant 33770 vvdifopab 34360 inxprnres 34396 relinxp 34405 dvhopellsm 36920 dibvalrel 36966 dib1dim 36968 diclspsn 36997 dih1 37089 dih1dimatlem 37132 aoprssdm 41796 eliunxp2 42630 |
Copyright terms: Public domain | W3C validator |