![]() |
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 5691 | . 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V) | |
2 | df-rel 5682 | . 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V)) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ Rel (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3474 ⊆ wss 3947 × cxp 5673 Rel wrel 5680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3954 df-ss 3964 df-opab 5210 df-xp 5681 df-rel 5682 |
This theorem is referenced by: xpsspw 5807 relinxp 5812 xpiindi 5833 eliunxp 5835 opeliunxp2 5836 relres 6008 restidsing 6050 codir 6118 qfto 6119 difxp 6160 sofld 6183 cnvcnv 6188 dfco2 6241 unixp 6278 ressn 6281 fliftcnv 7304 fliftfun 7305 oprssdm 7584 frxp 8108 frxp2 8126 frxp3 8133 opeliunxp2f 8191 reltpos 8212 tposfo 8234 tposf 8235 swoer 8729 xpider 8778 xpcomf1o 9057 fpwwe2lem8 10629 ordpinq 10934 addassnq 10949 mulassnq 10950 distrnq 10952 mulidnq 10954 recmulnq 10955 ltexnq 10966 prcdnq 10984 ltrel 11272 lerel 11274 dfle2 13122 fsumcom2 15716 fprodcom2 15924 0rest 17371 firest 17374 2oppchomf 17666 isinv 17703 invsym2 17706 invfun 17707 oppcsect2 17722 oppcinv 17723 oppchofcl 18209 oyoncl 18219 clatl 18457 gicer 19144 gsum2d2lem 19835 gsum2d2 19836 gsumcom2 19837 gsumxp 19838 dprd2d2 19908 mattpostpos 21947 mdetunilem9 22113 restbas 22653 txuni2 23060 txcls 23099 txdis1cn 23130 txkgen 23147 hmpher 23279 cnextrel 23558 tgphaus 23612 qustgplem 23616 tsmsxp 23650 utop2nei 23746 utop3cls 23747 xmeter 23930 caubl 24816 ovoliunlem1 25010 reldv 25378 taylf 25864 lgsquadlem1 26872 lgsquadlem2 26873 nvrel 29842 dfcnv2 31888 gsumpart 32194 qusxpid 32463 opprabs 32584 qtophaus 32804 cvmliftlem1 34264 cvmlift2lem12 34293 gonan0 34371 xpab 34683 dfso2 34713 relbigcup 34857 poimirlem3 36479 heicant 36511 vvdifopab 37116 cnvref4 37207 dvhopellsm 39976 dibvalrel 40022 dib1dim 40024 diclspsn 40053 dih1 40145 dih1dimatlem 40188 aoprssdm 45896 eliunxp2 46962 joindm2 47554 meetdm2 47556 |
Copyright terms: Public domain | W3C validator |