This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )