| 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 5637 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 × cxp 5614 |
| 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 5154 df-xp 5622 |
| This theorem is referenced by: xpriindi 5776 csbres 5931 fconstg 6710 curry2 8037 fparlem4 8045 xpord2pred 8075 xpord3pred 8082 naddcllem 8591 fvdiagfn 8815 mapsncnv 8817 xpsneng 8975 axdc4lem 10346 fpwwe2lem12 10533 expval 13970 imasvscafn 17441 fuchom 17871 homafval 17936 setcmon 17994 pwsco2mhm 18741 frmdplusg 18762 smndex1igid 18812 mulgfval 18982 mulgfvalALT 18983 mulgval 18984 efgval 19630 rngqipbas 21233 pzriprnglem13 21431 pzriprnglem14 21432 pjfval 21644 frlmval 21686 islindf5 21777 psrplusg 21874 psrvscafval 21886 psrvsca 21887 opsrle 21983 evlssca 22025 mpfind 22043 coe1fv 22120 coe1tm 22188 pf1ind 22271 mdetunilem4 22531 mdetunilem9 22536 txindislem 23549 txcmplem2 23558 txhaus 23563 txkgen 23568 xkofvcn 23600 xkoinjcn 23603 cnextval 23977 cnextfval 23978 pcorev2 24956 pcophtb 24957 pi1grplem 24977 pi1inv 24980 dvfval 25826 dvnfval 25852 0dgrb 26179 dgrnznn 26180 dgreq0 26199 dgrmulc 26205 plyrem 26241 facth 26242 fta1 26244 aaliou2 26276 taylfval 26294 taylpfval 26300 expsval 28349 0ofval 30765 2ndresdju 32629 aciunf1 32643 hashxpe 32787 indval2 32833 gsumpart 33035 ply1degltdimlem 33633 extdgfialglem1 33703 sxbrsigalem3 34283 sxbrsigalem2 34297 eulerpartlemgu 34388 sseqval 34399 sconnpht 35271 sconnpht2 35280 sconnpi1 35281 cvmlift2lem11 35355 cvmlift2lem12 35356 cvmlift2lem13 35357 cvmlift3lem9 35369 sat1el2xp 35421 mexval 35544 mexval2 35545 mdvval 35546 mpstval 35577 elima4 35818 bj-xtageq 37028 matunitlindflem1 37662 poimirlem32 37698 ismrer1 37884 lflsc0N 39128 lkrscss 39143 lfl1dim 39166 lfl1dim2N 39167 ldualvs 39182 evlsvvval 42602 evlsevl 42610 0prjspnrel 42666 mzpclval 42764 mzpcl1 42768 mendvsca 43226 dvconstbi 44373 expgrowth 44374 gpgov 48079 dmrnxp 48874 fucofvalne 49363 |
| Copyright terms: Public domain | W3C validator |