Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpeq2i | Structured version Visualization version GIF version |
Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.) |
Ref | Expression |
---|---|
xpeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
xpeq2i | ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | xpeq2 5610 | . 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: xpindir 5743 xpssres 5928 difxp1 6068 xpima 6085 xpexgALT 7824 curry1 7944 fparlem3 7954 fparlem4 7955 xp1en 8844 djuunxp 9679 dju1dif 9928 djuassen 9934 xpdjuen 9935 infdju1 9945 yonedalem3b 17997 yonedalem3 17998 pws1 19855 pwsmgp 19857 xkoinjcn 22838 imasdsf1olem 23526 df0op2 30114 ho01i 30190 nmop0h 30353 mbfmcst 32226 0rrv 32418 cvmlift2lem12 33276 zrdivrng 36111 |
Copyright terms: Public domain | W3C validator |