Theorem disjsn 4088

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 3869	. 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 4041	. . . . 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 1620	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1598	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2462	. . 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 1377   = wceq 1379   E.wex 1596   e. wcel 1767   i^i cin 3475   (/)c0 3785   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-dif 3479  df-in 3483  df-nul 3786  df-sn 4028

This theorem is referenced by:  disjsn2  4089  ssunsn2  4186  orddisj  4916  ndmima  5373  xpimasn  5452  funtpg  5638  fnunsn  5688  ressnop0  6068  ftpg  6071  funressn  6074  fsnunf  6099  fsnunfv  6101  domdifsn  7600  domunsncan  7617  map2xp  7687  limensuci  7693  infensuc  7695  php  7701  isinf  7733  ac6sfi  7764  fodomfi  7799  funsnfsupp  7853  infdifsn  8073  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  pm54.43  8381  dif1card  8388  numacn  8430  kmlem2  8531  cda1en  8555  ackbij1lem1  8600  ackbij1lem18  8617  fin23lem26  8705  isfin1-3  8766  axdc3lem4  8833  unsnen  8928  fpwwe2lem13  9020  ssxr  9654  fzpreddisj  11729  fzp1disj  11738  fzennn  12046  hashunsng  12427  hashxplem  12457  hashmap  12459  hashbclem  12467  hashf1lem1  12470  cats1un  12664  fsumsplitsnun  13533  fsum2dlem  13548  fsumabs  13578  fsumrlim  13588  fsumo1  13589  fsumiun  13598  isumltss  13623  bitsinv1  13951  bitsinvp1  13958  isprm2lem  14083  vdwmc2  14356  structcnvcnv  14501  strlemor1  14582  f1omvdco3  16280  psgnunilem5  16325  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzunsnd  16785  gsumunsnfd  16786  gsum2dlem2  16801  gsum2dOLD  16803  dprd2da  16893  ablfac1eulem  16925  ablfac1eu  16926  lbsextlem4  17607  fidomndrng  17755  mplmonmul  17925  psrbag0  17958  ist1-2  19642  xkohaus  19917  ptcmpfi  20077  flimsncls  20250  tmdgsum  20357  tsmsgsum  20400  tsmsgsumOLD  20403  restutopopn  20504  imasdsf1olem  20639  reconnlem1  21094  fsumcn  21137  ovolfiniun  21675  volfiniun  21720  ovolioo  21741  mbfconstlem  21799  i1fima2  21849  i1fd  21851  itg1val2  21854  itgfsum  21996  itgsplitioo  22007  dvmptfsum  22139  lhop1lem  22177  lhop  22180  vieta1lem2  22469  chtprm  23183  perfectlem2  23261  usgrares1  24114  nbgrassvwo  24141  nbgrassvwo2  24142  2pthlem2  24302  eupap1  24680  eupath2lem3  24683  vdegp1ai  24688  vdegp1bi  24689  ex-dif  24849  ex-in  24851  ofpreima2  27208  eulerpartlemt  27978  eulerpartgbij  27979  ballotlemfp1  28098  subfacp1lem5  28296  cvmliftlem4  28401  cvmliftlem5  28402  fprodm1  28701  fprod2dlem  28715  wfrlem13  28960  finixpnum  29643  locfindis  29805  mapfzcons2  30283  jm2.23  30570  kelac2lem  30642  kelac2  30643  pwslnm  30672  arearect  30816  volioc  31318  fsumsplitsndif  31841  bnj1421  33195  bj-disjcsn  33604  bj-xpimasn  33611  bj-xpima1snALT  33613