![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relxp | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpss 4919 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rel 4819 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbir 214 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-v 3015 df-in 3379 df-ss 3386 df-opab 4434 df-xp 4818 df-rel 4819 |
This theorem is referenced by: xpsspw 4926 xpiindi 4948 eliunxp 4950 opeliunxp2 4951 relres 5110 restidsing 5139 codir 5198 qfto 5199 difxp 5239 sofld 5262 cnvcnv 5267 dfco2 5313 unixp 5348 ressn 5351 fliftcnv 6190 fliftfun 6191 oprssdm 6438 frxp 6894 opeliunxp2f 6944 reltpos 6965 tpostpos 6980 tposfo 6987 tposf 6988 swoer 7378 xpider 7421 erinxp 7424 xpcomf1o 7648 cda1dif 8593 brdom3 8943 brdom5 8944 brdom4 8945 fpwwe2lem8 9049 fpwwe2lem9 9050 fpwwe2lem12 9053 ordpinq 9355 addassnq 9370 mulassnq 9371 distrnq 9373 mulidnq 9375 recmulnq 9376 ltexnq 9387 prcdnq 9405 ltrel 9683 lerel 9685 dfle2 11436 fsumcom2 13846 fprodcom2 14049 0rest 15339 firest 15342 pwsle 15401 2oppchomf 15640 isinv 15676 invsym2 15679 invfun 15680 oppcsect2 15695 oppcinv 15696 oppchofcl 16156 oyoncl 16166 clatl 16373 gicer 16951 gsum2d2lem 17616 gsum2d2 17617 gsumcom2 17618 gsumxp 17619 dprd2d2 17688 opsrtoslem2 18719 mattpostpos 19490 mdetunilem9 19656 restbas 20185 txuni2 20591 txcls 20630 txdis1cn 20661 txkgen 20678 hmpher 20810 cnextrel 21089 tgphaus 21142 qustgplem 21146 tsmsxp 21180 utop2nei 21276 utop3cls 21277 xmeter 21459 caubl 22288 ovoliunlem1 22466 reldv 22837 taylf 23328 lgsquadlem1 24294 lgsquadlem2 24295 nvrel 26233 dfcnv2 28287 qtophaus 28670 cvmliftlem1 30014 cvmlift2lem12 30043 dfso2 30400 elrn3 30409 relbigcup 30670 poimirlem3 31945 heicant 31977 dvhopellsm 34687 dibvalrel 34733 dib1dim 34735 diclspsn 34764 dih1 34856 dih1dimatlem 34899 aoprssdm 38795 eliunxp2 40440 |
Copyright terms: Public domain | W3C validator |