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 5149 | . 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V) | |
2 | df-rel 5045 | . 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V)) | |
3 | 1, 2 | mpbir 220 | 1 ⊢ Rel (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3173 ⊆ wss 3540 × cxp 5036 Rel wrel 5043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-opab 4644 df-xp 5044 df-rel 5045 |
This theorem is referenced by: xpsspw 5156 xpiindi 5179 eliunxp 5181 opeliunxp2 5182 relres 5346 restidsing 5377 restidsingOLD 5378 codir 5435 qfto 5436 difxp 5477 sofld 5500 cnvcnv 5505 dfco2 5551 unixp 5585 ressn 5588 fliftcnv 6461 fliftfun 6462 oprssdm 6713 frxp 7174 opeliunxp2f 7223 reltpos 7244 tpostpos 7259 tposfo 7266 tposf 7267 swoer 7659 xpider 7705 erinxp 7708 xpcomf1o 7934 cda1dif 8881 brdom3 9231 brdom5 9232 brdom4 9233 fpwwe2lem8 9338 fpwwe2lem9 9339 fpwwe2lem12 9342 ordpinq 9644 addassnq 9659 mulassnq 9660 distrnq 9662 mulidnq 9664 recmulnq 9665 ltexnq 9676 prcdnq 9694 ltrel 9979 lerel 9981 dfle2 11856 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 0rest 15913 firest 15916 pwsle 15975 2oppchomf 16207 isinv 16243 invsym2 16246 invfun 16247 oppcsect2 16262 oppcinv 16263 oppchofcl 16723 oyoncl 16733 clatl 16939 gicer 17541 gicerOLD 17542 gsum2d2lem 18195 gsum2d2 18196 gsumcom2 18197 gsumxp 18198 dprd2d2 18266 opsrtoslem2 19306 mattpostpos 20079 mdetunilem9 20245 restbas 20772 txuni2 21178 txcls 21217 txdis1cn 21248 txkgen 21265 hmpher 21397 cnextrel 21677 tgphaus 21730 qustgplem 21734 tsmsxp 21768 utop2nei 21864 utop3cls 21865 xmeter 22048 caubl 22914 ovoliunlem1 23077 reldv 23440 taylf 23919 lgsquadlem1 24905 lgsquadlem2 24906 nvrel 26841 dfcnv2 28859 qtophaus 29231 cvmliftlem1 30521 cvmlift2lem12 30550 dfso2 30897 elrn3 30906 relbigcup 31174 poimirlem3 32582 heicant 32614 dvhopellsm 35424 dibvalrel 35470 dib1dim 35472 diclspsn 35501 dih1 35593 dih1dimatlem 35636 aoprssdm 39931 eliunxp2 41905 |
Copyright terms: Public domain | W3C validator |