Metamath Proof Explorer


Theorem xpsndisj

Description: Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004)

Ref Expression
Assertion xpsndisj BDA×BC×D=

Proof

Step Hyp Ref Expression
1 disjsn2 BDBD=
2 xpdisj2 BD=A×BC×D=
3 1 2 syl BDA×BC×D=