![]() |
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 5367 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 × cxp 5344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-opab 4938 df-xp 5352 |
This theorem is referenced by: xpindir 5493 xpssres 5673 difxp1 5804 xpima 5821 xpexgALT 7426 curry1 7538 fparlem3 7548 fparlem4 7549 xp1en 8321 djuunxp 9067 xp2cda 9324 xpcdaen 9327 pwcda1 9338 pwcdandom 9811 yonedalem3b 17279 yonedalem3 17280 pws1 18977 pwsmgp 18979 xkoinjcn 21868 imasdsf1olem 22555 df0op2 29162 ho01i 29238 nmop0h 29401 mbfmcst 30862 0rrv 31055 cvmlift2lem12 31838 zrdivrng 34293 |
Copyright terms: Public domain | W3C validator |