| 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 5706 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-xp 5691 |
| This theorem is referenced by: xpriindi 5847 csbres 6000 fconstg 6795 curry2 8132 fparlem4 8140 xpord2pred 8170 xpord3pred 8177 naddcllem 8714 fvdiagfn 8931 mapsncnv 8933 xpsneng 9096 axdc4lem 10495 fpwwe2lem12 10682 expval 14104 imasvscafn 17582 fuchom 18009 homafval 18074 setcmon 18132 pwsco2mhm 18846 frmdplusg 18867 smndex1igid 18917 mulgfval 19087 mulgfvalALT 19088 mulgval 19089 efgval 19735 rngqipbas 21305 pzriprnglem13 21504 pzriprnglem14 21505 pjfval 21726 frlmval 21768 islindf5 21859 psrplusg 21956 psrvscafval 21968 psrvsca 21969 opsrle 22065 evlssca 22113 mpfind 22131 coe1fv 22208 coe1tm 22276 pf1ind 22359 mdetunilem4 22621 mdetunilem9 22626 txindislem 23641 txcmplem2 23650 txhaus 23655 txkgen 23660 xkofvcn 23692 xkoinjcn 23695 cnextval 24069 cnextfval 24070 pcorev2 25061 pcophtb 25062 pi1grplem 25082 pi1inv 25085 dvfval 25932 dvnfval 25958 0dgrb 26285 dgrnznn 26286 dgreq0 26305 dgrmulc 26311 plyrem 26347 facth 26348 fta1 26350 aaliou2 26382 taylfval 26400 taylpfval 26406 expsval 28408 0ofval 30806 2ndresdju 32659 aciunf1 32673 hashxpe 32811 indval2 32839 gsumpart 33060 ply1degltdimlem 33673 sxbrsigalem3 34274 sxbrsigalem2 34288 eulerpartlemgu 34379 sseqval 34390 sconnpht 35234 sconnpht2 35243 sconnpi1 35244 cvmlift2lem11 35318 cvmlift2lem12 35319 cvmlift2lem13 35320 cvmlift3lem9 35332 sat1el2xp 35384 mexval 35507 mexval2 35508 mdvval 35509 mpstval 35540 elima4 35776 bj-xtageq 36989 matunitlindflem1 37623 poimirlem32 37659 ismrer1 37845 lflsc0N 39084 lkrscss 39099 lfl1dim 39122 lfl1dim2N 39123 ldualvs 39138 evlsvvval 42573 evlsevl 42581 0prjspnrel 42637 mzpclval 42736 mzpcl1 42740 mendvsca 43199 dvconstbi 44353 expgrowth 44354 gpgov 48001 fucofvalne 49020 |
| Copyright terms: Public domain | W3C validator |