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

Proof

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