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 5547 | . 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 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-opab 5094 df-xp 5532 |
This theorem is referenced by: xpindir 5678 xpssres 5863 difxp1 5998 xpima 6015 xpexgALT 7708 curry1 7826 fparlem3 7836 fparlem4 7837 xp1en 8653 djuunxp 9424 dju1dif 9673 djuassen 9679 xpdjuen 9680 infdju1 9690 yonedalem3b 17646 yonedalem3 17647 pws1 19489 pwsmgp 19491 xkoinjcn 22439 imasdsf1olem 23127 df0op2 29687 ho01i 29763 nmop0h 29926 mbfmcst 31796 0rrv 31988 cvmlift2lem12 32847 zrdivrng 35731 |
Copyright terms: Public domain | W3C validator |