This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underset{j \in A}{Disj} (\{j\} \times B)$

Step	Hyp	Ref	Expression
1		sndisj	$⊢ \underset{j \in A}{Disj} \{j\}$
2	1	a1i	$⊢ ⊤ \to \underset{j \in A}{Disj} \{j\}$
3	2	disjxp1	$⊢ ⊤ \to \underset{j \in A}{Disj} (\{j\} \times B)$
4	3	mptru	$⊢ \underset{j \in A}{Disj} (\{j\} \times B)$