![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq2d | Structured version Visualization version GIF 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 5540 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 × cxp 5517 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-opab 5093 df-xp 5525 |
This theorem is referenced by: xpriindi 5671 csbres 5821 fconstg 6540 curry2 7785 fparlem4 7793 fvdiagfn 8438 mapsncnv 8440 xpsneng 8585 axdc4lem 9866 fpwwe2lem13 10053 expval 13427 imasvscafn 16802 fuchom 17223 homafval 17281 setcmon 17339 pwsco2mhm 17989 frmdplusg 18011 smndex1igid 18061 mulgfval 18218 mulgfvalALT 18219 mulgval 18220 efgval 18835 pjfval 20395 frlmval 20437 islindf5 20528 psrplusg 20619 psrvscafval 20628 psrvsca 20629 opsrle 20715 evlssca 20761 mpfind 20779 coe1fv 20835 coe1tm 20902 pf1ind 20979 mdetunilem4 21220 mdetunilem9 21225 txindislem 22238 txcmplem2 22247 txhaus 22252 txkgen 22257 xkofvcn 22289 xkoinjcn 22292 cnextval 22666 cnextfval 22667 pcorev2 23633 pcophtb 23634 pi1grplem 23654 pi1inv 23657 dvfval 24500 dvnfval 24525 0dgrb 24843 dgrnznn 24844 dgreq0 24862 dgrmulc 24868 plyrem 24901 facth 24902 fta1 24904 aaliou2 24936 taylfval 24954 taylpfval 24960 0ofval 28570 2ndresdju 30411 aciunf1 30426 hashxpe 30555 gsumpart 30740 indval2 31383 sxbrsigalem3 31640 sxbrsigalem2 31654 eulerpartlemgu 31745 sseqval 31756 sconnpht 32589 sconnpht2 32598 sconnpi1 32599 cvmlift2lem11 32673 cvmlift2lem12 32674 cvmlift2lem13 32675 cvmlift3lem9 32687 sat1el2xp 32739 mexval 32862 mexval2 32863 mdvval 32864 mpstval 32895 elima4 33132 bj-xtageq 34424 matunitlindflem1 35053 poimirlem32 35089 ismrer1 35276 lflsc0N 36379 lkrscss 36394 lfl1dim 36417 lfl1dim2N 36418 ldualvs 36433 0prjspnrel 39613 mzpclval 39666 mzpcl1 39670 mendvsca 40135 dvconstbi 41038 expgrowth 41039 |
Copyright terms: Public domain | W3C validator |