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 Disj j A j × B

Proof

Step Hyp Ref Expression
1 sndisj Disj j A j
2 1 a1i Disj j A j
3 2 disjxp1 Disj j A j × B
4 3 mptru Disj j A j × B