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 e. A ( { j } X. B )

Proof

Step	Hyp	Ref	Expression
1		sndisj	|- Disj_ j e. A { j }
2	1	a1i	|- ( T. -> Disj_ j e. A { j } )
3	2	disjxp1	|- ( T. -> Disj_ j e. A ( { j } X. B ) )
4	3	mptru	|- Disj_ j e. A ( { j } X. B )