| 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 4008 | . 2 ⊢ 𝐴 ⊆ V | |
| 2 | ssv 4008 | . 2 ⊢ 𝐵 ⊆ V | |
| 3 | xpss12 5700 | . 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
| Colors of variables: wff setvar class |
| Syntax hints: Vcvv 3480 ⊆ wss 3951 × cxp 5683 |
| 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 |
| This theorem is referenced by: relxp 5703 copsex2ga 5817 eqbrrdva 5880 relrelss 6293 dff3 7120 eqopi 8050 op1steq 8058 dfoprab4 8080 infxpenlem 10053 nqerf 10970 uzrdgfni 13999 reltrclfv 15056 homarel 18081 relxpchom 18226 frmdplusg 18867 psdmul 22170 upxp 23631 ustrel 24220 utop2nei 24259 utop3cls 24260 fmucndlem 24300 metustrel 24565 xppreima2 32661 df1stres 32713 df2ndres 32714 f1od2 32732 fsuppcurry1 32736 fsuppcurry2 32737 fpwrelmap 32744 metideq 33892 metider 33893 pstmfval 33895 xpinpreima2 33906 tpr2rico 33911 esum2d 34094 dya2iocnrect 34283 mpstssv 35544 txprel 35880 elxp8 37372 mblfinlem1 37664 xrnrel 38374 dihvalrel 41281 rfovcnvf1od 44017 ovolval2lem 46658 sprsymrelfo 47484 |
| Copyright terms: Public domain | W3C validator |