![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq2d | Structured version Visualization version Unicode version |
Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Ref | Expression |
---|---|
xpeq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
xpeq2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | xpeq2 4871 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-opab 4478 df-xp 4862 |
This theorem is referenced by: xpriindi 4993 csbres 5130 fconstg 5797 curry2 6923 fparlem4 6931 fvdiagfn 7547 mapsncnv 7549 xpsneng 7688 xpcdaen 8644 axdc4lem 8916 fpwwe2lem13 9098 expval 12312 imasvscafn 15498 comfffval 15658 fuchom 15921 homafval 15979 setcmon 16037 xpccofval 16122 pwsco2mhm 16673 frmdplusg 16693 mulgfval 16814 mulgval 16815 symgplusg 17085 efgval 17422 psrplusg 18660 psrvscafval 18669 psrvsca 18670 opsrle 18754 evlssca 18800 mpfind 18814 coe1fv 18854 coe1tm 18921 pf1ind 18998 pjfval 19324 frlmval 19366 islindf5 19452 mdetunilem4 19695 mdetunilem9 19700 txindislem 20703 txcmplem2 20712 txhaus 20717 txkgen 20722 xkofvcn 20754 xkoinjcn 20757 cnextval 21131 cnextfval 21132 pcorev2 22114 pcophtb 22115 pi1grplem 22135 pi1inv 22138 dvfval 22908 dvnfval 22932 0dgrb 23256 dgrnznn 23257 dgreq0 23275 dgrmulc 23281 plyrem 23314 facth 23315 fta1 23317 aaliou2 23352 taylfval 23370 taylpfval 23376 gxval 26042 0ofval 26484 aciunf1 28317 indval2 28887 sxbrsigalem3 29144 sxbrsigalem2 29158 eulerpartlemgu 29260 sseqval 29271 sconpht 30002 sconpht2 30011 sconpi1 30012 cvmlift2lem11 30086 cvmlift2lem12 30087 cvmlift2lem13 30088 cvmlift3lem9 30100 mexval 30190 mexval2 30191 mdvval 30192 mpstval 30223 elima4 30471 bj-xtageq 31628 poimirlem32 32018 ismrer1 32216 lflsc0N 32695 lkrscss 32710 lfl1dim 32733 lfl1dim2N 32734 ldualvs 32749 mzpclval 35613 mzpcl1 35617 mendvsca 36103 dvconstbi 36728 expgrowth 36729 csbresgOLD 37257 |
Copyright terms: Public domain | W3C validator |