Theorem disjprsn

Description: The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021)

	Ref	Expression
Assertion	disjprsn	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐶 } = { 𝐶 , 𝐶 }
2	1	ineq2i	⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐶 } )
3		disjpr2	⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐶 } ) = ∅ )
4	3	anidms	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐶 } ) = ∅ )
5	2 4	eqtrid	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )