![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq1d | 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 |
---|---|
xpeq1d | ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | xpeq1 5157 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 × cxp 5141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-opab 4746 df-xp 5149 |
This theorem is referenced by: csbres 5431 xpssres 5469 curry1 7314 fparlem3 7324 fparlem4 7325 ixpsnf1o 7990 xpfi 8272 dfac5lem3 8986 dfac5lem4 8987 cdaassen 9042 hashxplem 13258 repsw1 13576 subgga 17779 gasubg 17781 sylow2blem2 18082 psrval 19410 mpfrcl 19566 evlsval 19567 mamufval 20239 mat1dimscm 20329 mdetunilem3 20468 mdetunilem4 20469 mdetunilem9 20474 txindislem 21484 txtube 21491 txcmplem1 21492 txhaus 21498 xkoinjcn 21538 pt1hmeo 21657 tsmsxplem1 22003 tsmsxplem2 22004 cnmpt2pc 22774 dchrval 25004 axlowdimlem15 25881 axlowdim 25886 0ofval 27770 esumcvg 30276 sxbrsigalem0 30461 sxbrsigalem3 30462 sxbrsigalem2 30476 ofcccat 30748 mexval2 31526 csbfinxpg 33355 poimirlem1 33540 poimirlem2 33541 poimirlem3 33542 poimirlem4 33543 poimirlem5 33544 poimirlem6 33545 poimirlem7 33546 poimirlem8 33547 poimirlem10 33549 poimirlem11 33550 poimirlem12 33551 poimirlem15 33554 poimirlem16 33555 poimirlem17 33556 poimirlem18 33557 poimirlem19 33558 poimirlem20 33559 poimirlem21 33560 poimirlem22 33561 poimirlem23 33562 poimirlem24 33563 poimirlem26 33565 poimirlem27 33566 poimirlem28 33567 poimirlem32 33571 sdclem1 33669 ismrer1 33767 ldualset 34730 dibval 36748 dibval3N 36752 dib0 36770 dihwN 36895 hdmap1fval 37403 mzpclval 37605 mendval 38070 |
Copyright terms: Public domain | W3C validator |