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 3588 | . 2 ⊢ 𝐴 ⊆ V | |
2 | ssv 3588 | . 2 ⊢ 𝐵 ⊆ V | |
3 | xpss12 5148 | . 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V)) | |
4 | 1, 2, 3 | mp2an 704 | 1 ⊢ (𝐴 × 𝐵) ⊆ (V × V) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3173 ⊆ wss 3540 × cxp 5036 |
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 |
This theorem is referenced by: relxp 5150 copsex2ga 5154 eqbrrdva 5213 relrelss 5576 dff3 6280 eqopi 7093 op1steq 7101 dfoprab4 7116 infxpenlem 8719 nqerf 9631 uzrdgfni 12619 reltrclfv 13606 homarel 16509 relxpchom 16644 frmdplusg 17214 upxp 21236 ustrel 21825 utop2nei 21864 utop3cls 21865 fmucndlem 21905 metustrel 22167 xppreima2 28830 df1stres 28864 df2ndres 28865 f1od2 28887 fpwrelmap 28896 metideq 29264 metider 29265 pstmfval 29267 xpinpreima2 29281 tpr2rico 29286 esum2d 29482 dya2iocnrect 29670 mpstssv 30690 txprel 31156 bj-elid2 32263 elxp8 32395 mblfinlem1 32616 dihvalrel 35586 rfovcnvf1od 37318 ovolval2lem 39533 |
Copyright terms: Public domain | W3C validator |