![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpss2 | Structured version Visualization version Unicode version |
Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
xpss2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3437 |
. 2
![]() ![]() ![]() ![]() | |
2 | xpss12 4945 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan 684 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-in 3397 df-ss 3404 df-opab 4455 df-xp 4845 |
This theorem is referenced by: xpdom3 7688 marypha1lem 7965 unctb 8653 axresscn 9590 imasvscafn 15521 imasvscaf 15523 xpsc0 15544 xpsc1 15545 gass 17033 gsum2d 17682 tx2cn 20702 txtube 20732 txcmplem1 20733 hausdiag 20737 xkoinjcn 20779 caussi 22345 dvfval 22931 issh2 26943 qtophaus 28737 2ndmbfm 29156 sxbrsigalem0 29166 cvmlift2lem9 30106 cvmlift2lem11 30108 filnetlem3 31107 trclexi 36298 cnvtrcl0 36304 ovolval5lem2 38593 ovnovollem1 38596 ovnovollem2 38597 |
Copyright terms: Public domain | W3C validator |