# Metamath Proof Explorer

## Theorem xpcan

Description: Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011)

Ref Expression
Assertion xpcan ${⊢}{C}\ne \varnothing \to \left({C}×{A}={C}×{B}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 xp11 ${⊢}\left({C}\ne \varnothing \wedge {A}\ne \varnothing \right)\to \left({C}×{A}={C}×{B}↔\left({C}={C}\wedge {A}={B}\right)\right)$
2 eqid ${⊢}{C}={C}$
3 2 biantrur ${⊢}{A}={B}↔\left({C}={C}\wedge {A}={B}\right)$
4 1 3 syl6bbr ${⊢}\left({C}\ne \varnothing \wedge {A}\ne \varnothing \right)\to \left({C}×{A}={C}×{B}↔{A}={B}\right)$
5 nne ${⊢}¬{A}\ne \varnothing ↔{A}=\varnothing$
6 simpr ${⊢}\left({C}\ne \varnothing \wedge {A}=\varnothing \right)\to {A}=\varnothing$
7 xpeq2 ${⊢}{A}=\varnothing \to {C}×{A}={C}×\varnothing$
8 xp0 ${⊢}{C}×\varnothing =\varnothing$
9 7 8 syl6eq ${⊢}{A}=\varnothing \to {C}×{A}=\varnothing$
10 9 eqeq1d ${⊢}{A}=\varnothing \to \left({C}×{A}={C}×{B}↔\varnothing ={C}×{B}\right)$
11 eqcom ${⊢}\varnothing ={C}×{B}↔{C}×{B}=\varnothing$
12 10 11 syl6bb ${⊢}{A}=\varnothing \to \left({C}×{A}={C}×{B}↔{C}×{B}=\varnothing \right)$
13 12 adantl ${⊢}\left({C}\ne \varnothing \wedge {A}=\varnothing \right)\to \left({C}×{A}={C}×{B}↔{C}×{B}=\varnothing \right)$
14 df-ne ${⊢}{C}\ne \varnothing ↔¬{C}=\varnothing$
15 xpeq0 ${⊢}{C}×{B}=\varnothing ↔\left({C}=\varnothing \vee {B}=\varnothing \right)$
16 orel1 ${⊢}¬{C}=\varnothing \to \left(\left({C}=\varnothing \vee {B}=\varnothing \right)\to {B}=\varnothing \right)$
17 15 16 syl5bi ${⊢}¬{C}=\varnothing \to \left({C}×{B}=\varnothing \to {B}=\varnothing \right)$
18 14 17 sylbi ${⊢}{C}\ne \varnothing \to \left({C}×{B}=\varnothing \to {B}=\varnothing \right)$
19 18 adantr ${⊢}\left({C}\ne \varnothing \wedge {A}=\varnothing \right)\to \left({C}×{B}=\varnothing \to {B}=\varnothing \right)$
20 13 19 sylbid ${⊢}\left({C}\ne \varnothing \wedge {A}=\varnothing \right)\to \left({C}×{A}={C}×{B}\to {B}=\varnothing \right)$
21 eqtr3 ${⊢}\left({A}=\varnothing \wedge {B}=\varnothing \right)\to {A}={B}$
22 6 20 21 syl6an ${⊢}\left({C}\ne \varnothing \wedge {A}=\varnothing \right)\to \left({C}×{A}={C}×{B}\to {A}={B}\right)$
23 5 22 sylan2b ${⊢}\left({C}\ne \varnothing \wedge ¬{A}\ne \varnothing \right)\to \left({C}×{A}={C}×{B}\to {A}={B}\right)$
24 xpeq2 ${⊢}{A}={B}\to {C}×{A}={C}×{B}$
25 23 24 impbid1 ${⊢}\left({C}\ne \varnothing \wedge ¬{A}\ne \varnothing \right)\to \left({C}×{A}={C}×{B}↔{A}={B}\right)$
26 4 25 pm2.61dan ${⊢}{C}\ne \varnothing \to \left({C}×{A}={C}×{B}↔{A}={B}\right)$