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

Proof

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