| 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 5701 | . 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V) | |
| 2 | df-rel 5692 | . 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V)) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ Rel (𝐴 × 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: Vcvv 3480 ⊆ wss 3951 × cxp 5683 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: xpsspw 5819 relinxp 5824 inxp 5842 xpiindi 5846 eliunxp 5848 opeliunxp2 5849 relres 6023 restidsing 6071 codir 6140 qfto 6141 difxp 6184 sofld 6207 cnvcnv 6212 dfco2 6265 unixp 6302 ressn 6305 fliftcnv 7331 fliftfun 7332 oprssdm 7614 frxp 8151 frxp2 8169 frxp3 8176 opeliunxp2f 8235 reltpos 8256 tposfo 8278 tposf 8279 swoer 8776 xpider 8828 xpcomf1o 9101 fpwwe2lem8 10678 ordpinq 10983 addassnq 10998 mulassnq 10999 distrnq 11001 mulidnq 11003 recmulnq 11004 ltexnq 11015 prcdnq 11033 ltrel 11323 lerel 11325 dfle2 13189 fsumcom2 15810 fprodcom2 16020 0rest 17474 firest 17477 2oppchomf 17767 isinv 17804 invsym2 17807 invfun 17808 oppcsect2 17823 oppcinv 17824 oppchofcl 18305 oyoncl 18315 clatl 18553 gicer 19295 gsum2d2lem 19991 gsum2d2 19992 gsumcom2 19993 gsumxp 19994 dprd2d2 20064 mattpostpos 22460 mdetunilem9 22626 restbas 23166 txuni2 23573 txcls 23612 txdis1cn 23643 txkgen 23660 hmpher 23792 cnextrel 24071 tgphaus 24125 qustgplem 24129 tsmsxp 24163 utop2nei 24259 utop3cls 24260 xmeter 24443 caubl 25342 ovoliunlem1 25537 reldv 25905 taylf 26402 lgsquadlem1 27424 lgsquadlem2 27425 noseqrdgfn 28312 nvrel 30621 dfcnv2 32686 gsumpart 33060 gsumwrd2dccat 33070 elrgspnsubrunlem2 33252 qusxpid 33391 opprabs 33510 qtophaus 33835 cvmliftlem1 35290 cvmlift2lem12 35319 gonan0 35397 xpab 35726 dfso2 35755 relbigcup 35898 poimirlem3 37630 heicant 37662 vvdifopab 38261 cnvref4 38351 dvhopellsm 41119 dibvalrel 41165 dib1dim 41167 diclspsn 41196 dih1 41288 dih1dimatlem 41331 aoprssdm 47214 gricrel 47888 grlicrel 47966 eliunxp2 48250 coxp 48744 tposresxp 48783 tposf1o 48784 tposideq2 48789 joindm2 48865 meetdm2 48867 reldmxpc 48952 |
| Copyright terms: Public domain | W3C validator |