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 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sndisj	⊢ Disj 𝑗 ∈ 𝐴 { 𝑗 }
2	1	a1i	⊢ ( ⊤ → Disj 𝑗 ∈ 𝐴 { 𝑗 } )
3	2	disjxp1	⊢ ( ⊤ → Disj 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
4	3	mptru	⊢ Disj 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )