Theorem disjsn 3924

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 3709	. 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 3879	. . . . 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 1613	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1591	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2429	. . 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 1360   = wceq 1362   E.wex 1589   e. wcel 1755   i^i cin 3315   (/)c0 3625   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-v 2964  df-dif 3319  df-in 3323  df-nul 3626  df-sn 3866

This theorem is referenced by:  disjsn2  3925  ssunsn2  4020  orddisj  4744  ndmima  5193  xpimasn  5271  funtpg  5456  fnunsn  5506  ressnop0  5876  ftpg  5879  funressn  5882  fsnunf  5903  fsnunfv  5905  domdifsn  7382  domunsncan  7399  map2xp  7469  limensuci  7475  infensuc  7477  php  7483  isinf  7514  ac6sfi  7544  fodomfi  7578  funsnfsupp  7632  infdifsn  7850  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  pm54.43  8158  dif1card  8165  numacn  8207  kmlem2  8308  cda1en  8332  ackbij1lem1  8377  ackbij1lem18  8394  fin23lem26  8482  isfin1-3  8543  axdc3lem4  8610  unsnen  8705  fpwwe2lem13  8796  ssxr  9431  fzp1disj  11499  fzennn  11773  hashunsng  12137  hashxplem  12178  hashmap  12180  hashbclem  12188  hashf1lem1  12191  cats1un  12353  fsum2dlem  13220  fsumabs  13246  fsumrlim  13256  fsumo1  13257  fsumiun  13266  isumltss  13293  bitsinv1  13620  bitsinvp1  13627  isprm2lem  13752  vdwmc2  14022  structcnvcnv  14167  strlemor1  14247  f1omvdco3  15934  psgnunilem5  15979  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumunsnd  16426  gsum2dlem2  16435  gsum2dOLD  16437  dprd2da  16514  ablfac1eulem  16546  ablfac1eu  16547  lbsextlem4  17163  fidomndrng  17300  mplmonmul  17476  psrbag0  17507  ist1-2  18792  xkohaus  19067  ptcmpfi  19227  flimsncls  19400  tmdgsum  19507  tsmsgsum  19550  tsmsgsumOLD  19553  restutopopn  19654  imasdsf1olem  19789  reconnlem1  20244  fsumcn  20287  ovolfiniun  20825  volfiniun  20869  ovolioo  20890  mbfconstlem  20948  i1fima2  20998  i1fd  21000  itg1val2  21003  itgfsum  21145  itgsplitioo  21156  dvmptfsum  21288  lhop1lem  21326  lhop  21329  vieta1lem2  21661  chtprm  22375  perfectlem2  22453  usgrares1  23145  2pthlem2  23317  eupap1  23419  eupath2lem3  23422  vdegp1ai  23427  vdegp1bi  23428  ex-dif  23452  ex-in  23454  ofpreima2  25808  gsumunsnf  26096  gsumle  26097  eulerpartlemt  26601  eulerpartgbij  26602  ballotlemfp1  26721  subfacp1lem5  26919  cvmliftlem4  27024  cvmliftlem5  27025  fprodm1  27323  fprod2dlem  27337  wfrlem13  27582  finixpnum  28255  locfindis  28418  mapfzcons2  28897  jm2.23  29187  kelac2lem  29259  kelac2  29260  pwslnm  29289  arearect  29433  fsumsplitsndif  30081  fsumsplitsnun  30085  nbgrassvwo  30119  nbgrassvwo2  30120  bnj1421  31732  bj-disjcsn  32020  bj-xpimasn  32027  bj-xpima1snALT  32029