![]() |
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 5457 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 × cxp 5441 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-opab 5025 df-xp 5449 |
This theorem is referenced by: csbres 5737 xpssres 5770 curry1 7655 fparlem3 7665 fparlem4 7666 ixpsnf1o 8350 xpfi 8635 dfac5lem3 9397 dfac5lem4 9398 hashxplem 13642 repsw1 13981 subgga 18171 gasubg 18173 sylow2blem2 18476 psrval 19830 mpfrcl 19985 evlsval 19986 mamufval 20678 mat1dimscm 20768 mdetunilem3 20907 mdetunilem4 20908 mdetunilem9 20913 txindislem 21925 txtube 21932 txcmplem1 21933 txhaus 21939 xkoinjcn 21979 pt1hmeo 22098 tsmsxplem1 22444 tsmsxplem2 22445 cnmpopc 23215 dchrval 25492 axlowdimlem15 26425 axlowdim 26430 0ofval 28255 hashxpe 30213 esumcvg 30962 sxbrsigalem0 31146 sxbrsigalem3 31147 sxbrsigalem2 31161 ofcccat 31430 lpadval 31564 lpadlem3 31566 mexval2 32358 csbfinxpg 34200 poimirlem1 34424 poimirlem2 34425 poimirlem3 34426 poimirlem4 34427 poimirlem5 34428 poimirlem6 34429 poimirlem7 34430 poimirlem8 34431 poimirlem10 34433 poimirlem11 34434 poimirlem12 34435 poimirlem15 34438 poimirlem16 34439 poimirlem17 34440 poimirlem18 34441 poimirlem19 34442 poimirlem20 34443 poimirlem21 34444 poimirlem22 34445 poimirlem23 34446 poimirlem24 34447 poimirlem26 34449 poimirlem27 34450 poimirlem28 34451 poimirlem32 34455 sdclem1 34550 ismrer1 34648 ldualset 35792 dibval 37809 dibval3N 37813 dib0 37831 dihwN 37956 hdmap1fval 38463 mzpclval 38807 mendval 39268 |
Copyright terms: Public domain | W3C validator |