| 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 5632 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 × cxp 5609 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-opab 5149 df-xp 5617 |
| This theorem is referenced by: xpriindi 5771 csbres 5926 fconstg 6705 curry2 8032 fparlem4 8040 xpord2pred 8070 xpord3pred 8077 naddcllem 8586 fvdiagfn 8810 mapsncnv 8812 xpsneng 8970 axdc4lem 10341 fpwwe2lem12 10528 expval 13965 imasvscafn 17436 fuchom 17866 homafval 17931 setcmon 17989 pwsco2mhm 18736 frmdplusg 18757 smndex1igid 18807 mulgfval 18977 mulgfvalALT 18978 mulgval 18979 efgval 19624 rngqipbas 21227 pzriprnglem13 21425 pzriprnglem14 21426 pjfval 21638 frlmval 21680 islindf5 21771 psrplusg 21868 psrvscafval 21880 psrvsca 21881 opsrle 21977 evlssca 22019 mpfind 22037 coe1fv 22114 coe1tm 22182 pf1ind 22265 mdetunilem4 22525 mdetunilem9 22530 txindislem 23543 txcmplem2 23552 txhaus 23557 txkgen 23562 xkofvcn 23594 xkoinjcn 23597 cnextval 23971 cnextfval 23972 pcorev2 24950 pcophtb 24951 pi1grplem 24971 pi1inv 24974 dvfval 25820 dvnfval 25846 0dgrb 26173 dgrnznn 26174 dgreq0 26193 dgrmulc 26199 plyrem 26235 facth 26236 fta1 26238 aaliou2 26270 taylfval 26288 taylpfval 26294 expsval 28343 0ofval 30759 2ndresdju 32623 aciunf1 32637 hashxpe 32781 indval2 32827 gsumpart 33029 ply1degltdimlem 33627 extdgfialglem1 33697 sxbrsigalem3 34277 sxbrsigalem2 34291 eulerpartlemgu 34382 sseqval 34393 sconnpht 35265 sconnpht2 35274 sconnpi1 35275 cvmlift2lem11 35349 cvmlift2lem12 35350 cvmlift2lem13 35351 cvmlift3lem9 35363 sat1el2xp 35415 mexval 35538 mexval2 35539 mdvval 35540 mpstval 35571 elima4 35812 bj-xtageq 37022 matunitlindflem1 37656 poimirlem32 37692 ismrer1 37878 lflsc0N 39122 lkrscss 39137 lfl1dim 39160 lfl1dim2N 39161 ldualvs 39176 evlsvvval 42596 evlsevl 42604 0prjspnrel 42660 mzpclval 42758 mzpcl1 42762 mendvsca 43220 dvconstbi 44367 expgrowth 44368 gpgov 48073 dmrnxp 48868 fucofvalne 49357 |
| Copyright terms: Public domain | W3C validator |