Theorem disjsn 3684

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.)

Assertion

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

Proof of Theorem disjsn

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		disj1 3501	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 670	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3639	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 238	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 691	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 206	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1484	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1513	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2192	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 684	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 206	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1362   = wceq 1364   E.wex 1506   e. wcel 2167   i^i cin 3156   (/)c0 3450   {csn 3622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-dif 3159  df-in 3163  df-nul 3451  df-sn 3628

This theorem is referenced by:  disjsn2  3685  ssdifsn  3750  orddisj  4582  ndmima  5046  funtpg  5309  fnunsn  5365  ressnop0  5743  ftpg  5746  fsnunf  5762  fsnunfv  5763  enpr2d  6876  phpm  6926  fiunsnnn  6942  ac6sfi  6959  unsnfi  6980  tpfidisj  6990  iunfidisj  7012  pm54.43  7257  dju1en  7280  fzpreddisj  10146  fzp1disj  10155  frecfzennn  10518  hashunsng  10899  hashxp  10918  fsumsplitsn  11575  sumtp  11579  fsumsplitsnun  11584  fsum2dlemstep  11599  fsumconst  11619  fsumabs  11630  fsumiun  11642  fprodm1  11763  fprodunsn  11769  fprod2dlemstep  11787  fprodsplitsn  11798  ennnfonelemhf1o  12630  structcnvcnv  12694  fsumcncntop  14803  dvmptfsum  14961  perfectlem2  15236