Theorem disjsn

Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

	Ref	Expression
Assertion	disjsn	|- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Proof

Step	Hyp	Ref	Expression
1		disj1	|- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b	|- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn	|- ( x e. { B } <-> x = B )
4	3	imbi1i	|- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan	|- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2 4 5	3bitri	|- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii	|- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex	|- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		dfclel	|- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8 9	xchbinxr	|- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1 7 10	3bitri	|- ( ( A i^i { B } ) = (/) <-> -. B e. A )