Theorem disjsn 3728

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 3542	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 673	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3683	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 238	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 694	. . . 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 1516	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1545	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2225	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 687	. 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 1393   = wceq 1395   E.wex 1538   e. wcel 2200   i^i cin 3196   (/)c0 3491   {csn 3666

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-dif 3199  df-in 3203  df-nul 3492  df-sn 3672

This theorem is referenced by:  disjsn2  3729  ssdifsn  3796  opwo0id  4335  orddisj  4638  ndmima  5105  funtpg  5372  fnunsn  5430  ressnop0  5820  ftpg  5823  fsnunf  5839  fsnunfv  5840  enpr2d  6972  phpm  7027  fiunsnnn  7043  ac6sfi  7060  unsnfi  7081  tpfidisj  7091  iunfidisj  7113  pm54.43  7363  dju1en  7395  fzpreddisj  10267  fzp1disj  10276  frecfzennn  10648  hashunsng  11029  hashxp  11048  fsumsplitsn  11921  sumtp  11925  fsumsplitsnun  11930  fsum2dlemstep  11945  fsumconst  11965  fsumabs  11976  fsumiun  11988  fprodm1  12109  fprodunsn  12115  fprod2dlemstep  12133  fprodsplitsn  12144  bitsinv1  12473  ennnfonelemhf1o  12984  structcnvcnv  13048  fsumcncntop  15241  dvmptfsum  15399  perfectlem2  15674