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 3625 | . 2 ⊢ 𝐴 ⊆ V | |
2 | ssv 3625 | . 2 ⊢ 𝐵 ⊆ V | |
3 | xpss12 5225 | . 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V)) | |
4 | 1, 2, 3 | mp2an 708 | 1 ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3200 ⊆ wss 3574 × cxp 5112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 df-opab 4713 df-xp 5120 |
This theorem is referenced by: relxp 5227 copsex2ga 5231 eqbrrdva 5291 relrelss 5659 dff3 6372 eqopi 7202 op1steq 7210 dfoprab4 7225 infxpenlem 8836 nqerf 9752 uzrdgfni 12757 reltrclfv 13758 homarel 16686 relxpchom 16821 frmdplusg 17391 upxp 21426 ustrel 22015 utop2nei 22054 utop3cls 22055 fmucndlem 22095 metustrel 22357 xppreima2 29450 df1stres 29481 df2ndres 29482 f1od2 29499 fpwrelmap 29508 metideq 29936 metider 29937 pstmfval 29939 xpinpreima2 29953 tpr2rico 29958 esum2d 30155 dya2iocnrect 30343 mpstssv 31436 txprel 31986 bj-elid2 33086 elxp8 33219 mblfinlem1 33446 xrnrel 34136 dihvalrel 36568 rfovcnvf1od 38298 ovolval2lem 40857 sprsymrelfo 41747 |
Copyright terms: Public domain | W3C validator |