Theorem disjsn 3685

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 3502	. 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 3640	. . . . 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 3451   {csn 3623

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 3452  df-sn 3629

This theorem is referenced by:  disjsn2  3686  ssdifsn  3751  orddisj  4583  ndmima  5047  funtpg  5310  fnunsn  5368  ressnop0  5746  ftpg  5749  fsnunf  5765  fsnunfv  5766  enpr2d  6885  phpm  6935  fiunsnnn  6951  ac6sfi  6968  unsnfi  6989  tpfidisj  6999  iunfidisj  7021  pm54.43  7269  dju1en  7296  fzpreddisj  10163  fzp1disj  10172  frecfzennn  10535  hashunsng  10916  hashxp  10935  fsumsplitsn  11592  sumtp  11596  fsumsplitsnun  11601  fsum2dlemstep  11616  fsumconst  11636  fsumabs  11647  fsumiun  11659  fprodm1  11780  fprodunsn  11786  fprod2dlemstep  11804  fprodsplitsn  11815  bitsinv1  12144  ennnfonelemhf1o  12655  structcnvcnv  12719  fsumcncntop  14887  dvmptfsum  15045  perfectlem2  15320