Theorem disjsn 4057

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 3835	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 335	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		elsn 4010	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 326	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 423	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 274	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1687	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1661	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2417	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 312	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 274	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   i^i cin 3435   (/)c0 3761   {csn 3996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-v 3083  df-dif 3439  df-in 3443  df-nul 3762  df-sn 3997

This theorem is referenced by:  disjsn2  4058  ssunsn2  4156  ndmima  5221  ndmimaOLD  5222  xpimasn  5298  orddisj  5477  funtpg  5648  fnunsn  5698  ressnop0  6083  ftpg  6086  funressn  6089  fsnunf  6114  fsnunfv  6116  wfrlem13  7053  domdifsn  7658  domunsncan  7675  map2xp  7745  limensuci  7751  infensuc  7753  php  7759  isinf  7788  ac6sfi  7818  fodomfi  7853  funsnfsupp  7910  infdifsn  8164  cantnfp1lem3  8187  pm54.43  8436  dif1card  8443  numacn  8481  kmlem2  8582  cda1en  8606  ackbij1lem1  8651  ackbij1lem18  8668  fin23lem26  8756  isfin1-3  8817  axdc3lem4  8884  unsnen  8979  fpwwe2lem13  9068  ssxr  9704  fzpreddisj  11846  fzp1disj  11855  fzennn  12181  hashunsng  12571  hashxplem  12603  hashmap  12605  hashbclem  12613  hashf1lem1  12616  cats1un  12823  sumtp  13798  fsumsplitsnun  13804  fsum2dlem  13819  fsumabs  13849  fsumrlim  13859  fsumo1  13860  fsumiun  13869  isumltss  13894  fprodm1  14009  fprod2dlem  14022  fprodsplitsn  14031  fproddvdsd  14358  bitsinv1  14404  bitsinvp1  14411  isprm2lem  14619  vdwmc2  14917  prmdvdsprmo  14988  prmdvdsprmorOLD  15003  structcnvcnv  15120  strlemor1  15205  f1omvdco3  17078  psgnunilem5  17123  gsumzaddlem  17542  gsumzunsnd  17576  gsumunsnfd  17577  gsum2dlem2  17591  dprd2da  17663  ablfac1eulem  17693  ablfac1eu  17694  lbsextlem4  18372  fidomndrng  18519  mplmonmul  18676  psrbag0  18705  ist1-2  20350  locfindis  20532  xkohaus  20655  ptcmpfi  20815  flimsncls  20988  tmdgsum  21097  tsmsgsum  21140  imasdsf1olem  21375  reconnlem1  21831  fsumcn  21889  ovolfiniun  22441  volfiniun  22487  ovolioo  22508  mbfconstlem  22572  i1fima2  22624  i1fd  22626  itg1val2  22629  itgfsum  22771  itgsplitioo  22782  dvmptfsum  22914  lhop1lem  22952  lhop  22955  vieta1lem2  23251  chtprm  24067  perfectlem2  24145  usgrares1  25124  nbgrassvwo  25151  nbgrassvwo2  25152  2pthlem2  25312  eupap1  25690  eupath2lem3  25693  vdegp1ai  25698  vdegp1bi  25699  ex-dif  25859  ex-in  25861  ofpreima2  28259  padct  28301  fzdif2  28363  esumrnmpt2  28885  esum2dlem  28909  carsgclctunlem1  29145  eulerpartlemt  29200  eulerpartgbij  29201  ballotlemfp1  29320  bnj1421  29847  subfacp1lem5  29903  cvmliftlem4  30007  cvmliftlem5  30008  mrsubvrs  30156  bj-disjcsn  31498  bj-xpimasn  31504  bj-xpima1snALT  31506  finixpnum  31844  poimirlem3  31857  poimirlem4  31858  poimirlem13  31867  poimirlem14  31868  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem18  31872  poimirlem19  31873  poimirlem20  31874  poimirlem21  31875  poimirlem22  31876  poimirlem27  31881  mapfzcons2  35480  jm2.23  35771  kelac2lem  35842  kelac2  35843  pwslnm  35872  arearect  36020  iunrelexp0  36154  disjiun2  37260  fsumsplitsn  37472  volioc  37669  sge0iunmptlemfi  38043  ismeannd  38084  volico  38138  perfectALTVlem2  38556  fsumsplitsndif  38756