Theorem disjprsn

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

	Ref	Expression
Assertion	disjprsn	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { C } = { C , C }
2	1	ineq2i	|- ( { A , B } i^i { C } ) = ( { A , B } i^i { C , C } )
3		disjpr2	|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= C /\ B =/= C ) ) -> ( { A , B } i^i { C , C } ) = (/) )
4	3	anidms	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C , C } ) = (/) )
5	2 4	eqtrid	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )