Metamath Proof Explorer


Theorem disjsnxp

Description: The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion disjsnxp DisjjAj×B

Proof

Step Hyp Ref Expression
1 sndisj DisjjAj
2 1 a1i DisjjAj
3 2 disjxp1 DisjjAj×B
4 3 mptru DisjjAj×B