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 5540 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 × cxp 5524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-opab 5094 df-xp 5532 |
This theorem is referenced by: iunxpconst 5596 xpindi 5677 difxp2 5999 resdmres 6065 xpprsng 6915 curry2 7831 mapsnconst 8505 mapsncnv 8506 xp2dju 9679 pwdju1 9693 pwdjundom 10170 geomulcvg 15327 hofcl 17628 evlsval 20903 matvsca2 21182 ehl0 24172 ovoliunnul 24262 vitalilem5 24367 lgam1 25804 finxp2o 35216 finxp3o 35217 poimirlem3 35426 poimirlem5 35428 poimirlem10 35433 poimirlem22 35445 poimirlem23 35446 mendvscafval 40610 binomcxplemnn0 41528 itscnhlinecirc02plem3 45694 inlinecirc02p 45697 |
Copyright terms: Public domain | W3C validator |