![]() |
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 5686 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 × cxp 5670 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-opab 5206 df-xp 5678 |
This theorem is referenced by: csbres 5982 xpssres 6017 curry1 8107 fparlem3 8117 fparlem4 8118 xpord2pred 8148 xpord3pred 8155 naddcllem 8695 ixpsnf1o 8956 xpfiOLD 9351 dfac5lem3 10158 dfac5lem4 10159 hashxplem 14442 repsw1 14783 subgga 19287 gasubg 19289 sylow2blem2 19612 psrval 21905 mpfrcl 22093 evlsval 22094 mamufval 22377 mat1dimscm 22462 mdetunilem3 22601 mdetunilem4 22602 mdetunilem9 22607 txindislem 23622 txtube 23629 txcmplem1 23630 txhaus 23636 xkoinjcn 23676 pt1hmeo 23795 tsmsxplem1 24142 tsmsxplem2 24143 cnmpopc 24934 dchrval 27257 axlowdimlem15 28884 axlowdim 28889 0ofval 30714 hashxpe 32711 erlval 33115 fracbas 33157 esumcvg 33929 sxbrsigalem0 34115 sxbrsigalem3 34116 sxbrsigalem2 34130 ofcccat 34399 lpadval 34532 lpadlem3 34534 mexval2 35341 csbfinxpg 37105 poimirlem1 37332 poimirlem2 37333 poimirlem3 37334 poimirlem4 37335 poimirlem5 37336 poimirlem6 37337 poimirlem7 37338 poimirlem8 37339 poimirlem10 37341 poimirlem11 37342 poimirlem12 37343 poimirlem15 37346 poimirlem16 37347 poimirlem17 37348 poimirlem18 37349 poimirlem19 37350 poimirlem20 37351 poimirlem21 37352 poimirlem22 37353 poimirlem23 37354 poimirlem24 37355 poimirlem26 37357 poimirlem27 37358 poimirlem28 37359 poimirlem32 37363 sdclem1 37454 ismrer1 37549 ldualset 38833 dibval 40851 dibval3N 40855 dib0 40873 dihwN 40998 hdmap1fval 41505 fsuppssind 42280 mzpclval 42416 mendval 42878 prstcval 48418 prstchomval 48428 |
Copyright terms: Public domain | W3C validator |