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 5603 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 × cxp 5587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-opab 5137 df-xp 5595 |
This theorem is referenced by: iunxpconst 5659 xpindi 5742 difxp2 6069 resdmres 6135 xpprsng 7012 curry2 7947 mapsnconst 8680 mapsncnv 8681 xp2dju 9932 pwdju1 9946 pwdjundom 10423 geomulcvg 15588 hofcl 17977 evlsval 21296 matvsca2 21577 ehl0 24581 ovoliunnul 24671 vitalilem5 24776 lgam1 26213 finxp2o 35570 finxp3o 35571 poimirlem3 35780 poimirlem5 35782 poimirlem10 35787 poimirlem22 35799 poimirlem23 35800 mendvscafval 41015 binomcxplemnn0 41967 itscnhlinecirc02plem3 46130 inlinecirc02p 46133 |
Copyright terms: Public domain | W3C validator |