![]() |
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 5701 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 × cxp 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-opab 5213 df-xp 5686 |
This theorem is referenced by: xpindir 5839 xpssres 6025 difxp1 6172 xpima 6189 xpexgALT 7989 curry1 8113 fparlem3 8123 fparlem4 8124 xp1en 9086 djuunxp 9950 dju1dif 10201 djuassen 10207 xpdjuen 10208 infdju1 10218 yonedalem3b 18276 yonedalem3 18277 pws1 20266 pwsmgp 20268 xkoinjcn 23609 imasdsf1olem 24297 df0op2 31580 ho01i 31656 nmop0h 31819 mbfmcst 33884 0rrv 34076 cvmlift2lem12 34929 zrdivrng 37431 |
Copyright terms: Public domain | W3C validator |