![]() |
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 5696 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 × cxp 5673 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-opab 5210 df-xp 5681 |
This theorem is referenced by: xpriindi 5834 csbres 5982 fconstg 6775 curry2 8089 fparlem4 8097 xpord2pred 8127 xpord3pred 8134 naddcllem 8671 fvdiagfn 8881 mapsncnv 8883 xpsneng 9052 axdc4lem 10446 fpwwe2lem12 10633 expval 14025 imasvscafn 17479 fuchom 17909 fuchomOLD 17910 homafval 17975 setcmon 18033 pwsco2mhm 18710 frmdplusg 18731 smndex1igid 18781 mulgfval 18946 mulgfvalALT 18947 mulgval 18948 efgval 19579 pjfval 21252 frlmval 21294 islindf5 21385 psrplusg 21491 psrvscafval 21500 psrvsca 21501 opsrle 21593 evlssca 21643 mpfind 21661 coe1fv 21721 coe1tm 21786 pf1ind 21865 mdetunilem4 22108 mdetunilem9 22113 txindislem 23128 txcmplem2 23137 txhaus 23142 txkgen 23147 xkofvcn 23179 xkoinjcn 23182 cnextval 23556 cnextfval 23557 pcorev2 24535 pcophtb 24536 pi1grplem 24556 pi1inv 24559 dvfval 25405 dvnfval 25430 0dgrb 25751 dgrnznn 25752 dgreq0 25770 dgrmulc 25776 plyrem 25809 facth 25810 fta1 25812 aaliou2 25844 taylfval 25862 taylpfval 25868 0ofval 30027 2ndresdju 31861 aciunf1 31875 hashxpe 32006 gsumpart 32194 ply1degltdimlem 32695 indval2 33000 sxbrsigalem3 33259 sxbrsigalem2 33273 eulerpartlemgu 33364 sseqval 33375 sconnpht 34208 sconnpht2 34217 sconnpi1 34218 cvmlift2lem11 34292 cvmlift2lem12 34293 cvmlift2lem13 34294 cvmlift3lem9 34306 sat1el2xp 34358 mexval 34481 mexval2 34482 mdvval 34483 mpstval 34514 elima4 34735 bj-xtageq 35857 matunitlindflem1 36472 poimirlem32 36508 ismrer1 36694 lflsc0N 37941 lkrscss 37956 lfl1dim 37979 lfl1dim2N 37980 ldualvs 37995 evlsvvval 41132 evlsevl 41140 0prjspnrel 41365 mzpclval 41448 mzpcl1 41452 mendvsca 41918 dvconstbi 43078 expgrowth 43079 rngqipbas 46760 |
Copyright terms: Public domain | W3C validator |