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 3911 | . 2 ⊢ 𝐴 ⊆ V | |
2 | ssv 3911 | . 2 ⊢ 𝐵 ⊆ V | |
3 | xpss12 5551 | . 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V)) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3398 ⊆ wss 3853 × cxp 5534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-in 3860 df-ss 3870 df-opab 5102 df-xp 5542 |
This theorem is referenced by: relxp 5554 copsex2ga 5662 eqbrrdva 5723 relrelss 6116 dff3 6897 eqopi 7775 op1steq 7783 dfoprab4 7803 infxpenlem 9592 nqerf 10509 uzrdgfni 13496 reltrclfv 14545 homarel 17496 relxpchom 17642 frmdplusg 18235 upxp 22474 ustrel 23063 utop2nei 23102 utop3cls 23103 fmucndlem 23142 metustrel 23404 xppreima2 30661 df1stres 30710 df2ndres 30711 f1od2 30730 fsuppcurry1 30734 fsuppcurry2 30735 fpwrelmap 30742 metideq 31511 metider 31512 pstmfval 31514 xpinpreima2 31525 tpr2rico 31530 esum2d 31727 dya2iocnrect 31914 mpstssv 33168 txprel 33867 elxp8 35228 mblfinlem1 35500 xrnrel 36189 dihvalrel 38979 rfovcnvf1od 41230 ovolval2lem 43799 sprsymrelfo 44565 |
Copyright terms: Public domain | W3C validator |