Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpss | Structured version Visualization version GIF version |
Description: A Cartesian product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
xpss | ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssv 3988 | . 2 ⊢ 𝐴 ⊆ V | |
2 | ssv 3988 | . 2 ⊢ 𝐵 ⊆ V | |
3 | xpss12 5563 | . 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V)) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3492 ⊆ wss 3933 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-ss 3949 df-opab 5120 df-xp 5554 |
This theorem is referenced by: relxp 5566 copsex2ga 5673 eqbrrdva 5733 relrelss 6117 dff3 6858 eqopi 7714 op1steq 7722 dfoprab4 7742 infxpenlem 9427 nqerf 10340 uzrdgfni 13314 reltrclfv 14365 homarel 17284 relxpchom 17419 frmdplusg 18007 upxp 22159 ustrel 22747 utop2nei 22786 utop3cls 22787 fmucndlem 22827 metustrel 23089 xppreima2 30323 df1stres 30365 df2ndres 30366 f1od2 30383 fsuppcurry1 30387 fsuppcurry2 30388 fpwrelmap 30395 metideq 31032 metider 31033 pstmfval 31035 xpinpreima2 31049 tpr2rico 31054 esum2d 31251 dya2iocnrect 31438 mpstssv 32683 txprel 33237 elxp8 34534 mblfinlem1 34810 xrnrel 35505 dihvalrel 38295 rfovcnvf1od 40228 ovolval2lem 42802 sprsymrelfo 43536 |
Copyright terms: Public domain | W3C validator |