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  4336  orddisj  4639  ndmima  5108  funtpg  5375  fnunsn  5433  ressnop0  5827  ftpg  5830  fsnunf  5846  fsnunfv  5847  enpr2d  6985  phpm  7040  fiunsnnn  7056  ac6sfi  7073  unsnfi  7097  tpfidisj  7107  iunfidisj  7129  pm54.43  7379  dju1en  7411  fzpreddisj  10284  fzp1disj  10293  frecfzennn  10665  hashunsng  11047  hashxp  11066  fsumsplitsn  11942  sumtp  11946  fsumsplitsnun  11951  fsum2dlemstep  11966  fsumconst  11986  fsumabs  11997  fsumiun  12009  fprodm1  12130  fprodunsn  12136  fprod2dlemstep  12154  fprodsplitsn  12165  bitsinv1  12494  ennnfonelemhf1o  13005  structcnvcnv  13069  fsumcncntop  15262  dvmptfsum  15420  perfectlem2  15695