|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > xpeq1i | Structured version Visualization version GIF version | ||
| Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.) | 
| Ref | Expression | 
|---|---|
| xpeq1i.1 | ⊢ 𝐴 = 𝐵 | 
| Ref | Expression | 
|---|---|
| xpeq1i | ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | xpeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | xpeq1 5698 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 × cxp 5682 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-opab 5205 df-xp 5690 | 
| This theorem is referenced by: iunxpconst 5757 xpindi 5843 difxp2 6185 resdmres 6251 xpprsng 7159 curry2 8133 mapsnconst 8933 mapsncnv 8934 xp2dju 10218 pwdju1 10232 pwdjundom 10708 geomulcvg 15913 hofcl 18305 evlsval 22111 matvsca2 22435 ehl0 25452 ovoliunnul 25543 vitalilem5 25648 lgam1 27108 iunxpssiun1 32582 finxp2o 37401 finxp3o 37402 poimirlem3 37631 poimirlem5 37633 poimirlem10 37638 poimirlem22 37650 poimirlem23 37651 mendvscafval 43203 binomcxplemnn0 44373 itscnhlinecirc02plem3 48710 inlinecirc02p 48713 | 
| Copyright terms: Public domain | W3C validator |