Theorem disjsn 3935

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 3720	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 334	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		elsn 3890	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 325	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 422	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 271	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1610	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1588	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2438	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 311	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 271	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   i^i cin 3326   (/)c0 3636   {csn 3876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2719  df-v 2973  df-dif 3330  df-in 3334  df-nul 3637  df-sn 3877

This theorem is referenced by:  disjsn2  3936  ssunsn2  4031  orddisj  4756  ndmima  5204  xpimasn  5282  funtpg  5467  fnunsn  5517  ressnop0  5888  ftpg  5891  funressn  5894  fsnunf  5915  fsnunfv  5917  domdifsn  7393  domunsncan  7410  map2xp  7480  limensuci  7486  infensuc  7488  php  7494  isinf  7525  ac6sfi  7555  fodomfi  7589  funsnfsupp  7643  infdifsn  7861  cantnfp1lem3  7887  cantnfp1lem3OLD  7913  pm54.43  8169  dif1card  8176  numacn  8218  kmlem2  8319  cda1en  8343  ackbij1lem1  8388  ackbij1lem18  8405  fin23lem26  8493  isfin1-3  8554  axdc3lem4  8621  unsnen  8716  fpwwe2lem13  8808  ssxr  9443  fzpreddisj  11503  fzp1disj  11514  fzennn  11789  hashunsng  12153  hashxplem  12194  hashmap  12196  hashbclem  12204  hashf1lem1  12207  cats1un  12369  fsum2dlem  13236  fsumabs  13263  fsumrlim  13273  fsumo1  13274  fsumiun  13283  isumltss  13310  bitsinv1  13637  bitsinvp1  13644  isprm2lem  13769  vdwmc2  14039  structcnvcnv  14184  strlemor1  14264  f1omvdco3  15954  psgnunilem5  15999  gsumzaddlem  16407  gsumzaddlemOLD  16409  gsumzunsnd  16450  gsumunsnd  16451  gsum2dlem2  16461  gsum2dOLD  16463  dprd2da  16540  ablfac1eulem  16572  ablfac1eu  16573  lbsextlem4  17241  fidomndrng  17378  mplmonmul  17542  psrbag0  17575  ist1-2  18950  xkohaus  19225  ptcmpfi  19385  flimsncls  19558  tmdgsum  19665  tsmsgsum  19708  tsmsgsumOLD  19711  restutopopn  19812  imasdsf1olem  19947  reconnlem1  20402  fsumcn  20445  ovolfiniun  20983  volfiniun  21027  ovolioo  21048  mbfconstlem  21106  i1fima2  21156  i1fd  21158  itg1val2  21161  itgfsum  21303  itgsplitioo  21314  dvmptfsum  21446  lhop1lem  21484  lhop  21487  vieta1lem2  21776  chtprm  22490  perfectlem2  22568  usgrares1  23322  2pthlem2  23494  eupap1  23596  eupath2lem3  23599  vdegp1ai  23604  vdegp1bi  23605  ex-dif  23629  ex-in  23631  ofpreima2  25984  gsumunsnf  26244  gsumle  26245  eulerpartlemt  26753  eulerpartgbij  26754  ballotlemfp1  26873  subfacp1lem5  27071  cvmliftlem4  27176  cvmliftlem5  27177  fprodm1  27476  fprod2dlem  27490  wfrlem13  27735  finixpnum  28412  locfindis  28575  mapfzcons2  29053  jm2.23  29343  kelac2lem  29415  kelac2  29416  pwslnm  29445  arearect  29589  fsumsplitsndif  30236  fsumsplitsnun  30240  nbgrassvwo  30274  nbgrassvwo2  30275  bnj1421  32031  bj-disjcsn  32438  bj-xpimasn  32445  bj-xpima1snALT  32447