Metamath Proof Explorer

Theorem xpeq0

Description: At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006)

Ref Expression
Assertion xpeq0 
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )

Proof

Step Hyp Ref Expression
1 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
2 1 necon2bbii 
 |-  ( ( A X. B ) = (/) <-> -. ( A =/= (/) /\ B =/= (/) ) )
3 ianor 
 |-  ( -. ( A =/= (/) /\ B =/= (/) ) <-> ( -. A =/= (/) \/ -. B =/= (/) ) )
4 nne 
 |-  ( -. A =/= (/) <-> A = (/) )
5 nne 
 |-  ( -. B =/= (/) <-> B = (/) )
6 4 5 orbi12i 
 |-  ( ( -. A =/= (/) \/ -. B =/= (/) ) <-> ( A = (/) \/ B = (/) ) )
7 2 3 6 3bitri 
 |-  ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )