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 5569 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-opab 5120 df-xp 5554 |
This theorem is referenced by: xpriindi 5700 csbres 5849 fconstg 6559 curry2 7791 fparlem4 7799 fvdiagfn 8443 mapsncnv 8445 xpsneng 8590 axdc4lem 9865 fpwwe2lem13 10052 expval 13419 imasvscafn 16798 fuchom 17219 homafval 17277 setcmon 17335 pwsco2mhm 17985 frmdplusg 18007 mulgfval 18164 mulgfvalALT 18165 mulgval 18166 efgval 18772 psrplusg 20089 psrvscafval 20098 psrvsca 20099 opsrle 20184 evlssca 20230 mpfind 20248 coe1fv 20302 coe1tm 20369 pf1ind 20446 pjfval 20778 frlmval 20820 islindf5 20911 mdetunilem4 21152 mdetunilem9 21157 txindislem 22169 txcmplem2 22178 txhaus 22183 txkgen 22188 xkofvcn 22220 xkoinjcn 22223 cnextval 22597 cnextfval 22598 pcorev2 23559 pcophtb 23560 pi1grplem 23580 pi1inv 23583 dvfval 24422 dvnfval 24446 0dgrb 24763 dgrnznn 24764 dgreq0 24782 dgrmulc 24788 plyrem 24821 facth 24822 fta1 24824 aaliou2 24856 taylfval 24874 taylpfval 24880 0ofval 28491 aciunf1 30336 hashxpe 30455 indval2 31172 sxbrsigalem3 31429 sxbrsigalem2 31443 eulerpartlemgu 31534 sseqval 31545 sconnpht 32373 sconnpht2 32382 sconnpi1 32383 cvmlift2lem11 32457 cvmlift2lem12 32458 cvmlift2lem13 32459 cvmlift3lem9 32471 sat1el2xp 32523 mexval 32646 mexval2 32647 mdvval 32648 mpstval 32679 elima4 32916 bj-xtageq 34197 matunitlindflem1 34769 poimirlem32 34805 ismrer1 34997 lflsc0N 36099 lkrscss 36114 lfl1dim 36137 lfl1dim2N 36138 ldualvs 36153 0prjspnrel 39147 mzpclval 39200 mzpcl1 39204 mendvsca 39669 dvconstbi 40543 expgrowth 40544 smndex1igid 44004 |
Copyright terms: Public domain | W3C validator |