Theorem disjsn 4075

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 3855	. 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 4028	. . . . 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 1627	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1601	. . 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 1381   = wceq 1383   E.wex 1599   e. wcel 1804   i^i cin 3460   (/)c0 3770   {csn 4014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097  df-dif 3464  df-in 3468  df-nul 3771  df-sn 4015

This theorem is referenced by:  disjsn2  4076  ssunsn2  4174  orddisj  4906  ndmima  5363  xpimasn  5442  funtpg  5628  fnunsn  5678  ressnop0  6063  ftpg  6066  funressn  6069  fsnunf  6094  fsnunfv  6096  domdifsn  7602  domunsncan  7619  map2xp  7689  limensuci  7695  infensuc  7697  php  7703  isinf  7735  ac6sfi  7766  fodomfi  7801  funsnfsupp  7855  infdifsn  8076  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  pm54.43  8384  dif1card  8391  numacn  8433  kmlem2  8534  cda1en  8558  ackbij1lem1  8603  ackbij1lem18  8620  fin23lem26  8708  isfin1-3  8769  axdc3lem4  8836  unsnen  8931  fpwwe2lem13  9023  ssxr  9657  fzpreddisj  11740  fzp1disj  11749  fzennn  12060  hashunsng  12441  hashxplem  12473  hashmap  12475  hashbclem  12483  hashf1lem1  12486  cats1un  12683  fsumsplitsnun  13552  fsum2dlem  13567  fsumabs  13597  fsumrlim  13607  fsumo1  13608  fsumiun  13617  isumltss  13642  fprodm1  13753  fprod2dlem  13766  bitsinv1  14074  bitsinvp1  14081  isprm2lem  14206  vdwmc2  14479  structcnvcnv  14625  strlemor1  14706  f1omvdco3  16453  psgnunilem5  16498  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumzunsnd  16961  gsumunsnfd  16962  gsum2dlem2  16977  gsum2dOLD  16979  dprd2da  17070  ablfac1eulem  17102  ablfac1eu  17103  lbsextlem4  17786  fidomndrng  17935  mplmonmul  18105  psrbag0  18138  ist1-2  19826  locfindis  20009  xkohaus  20132  ptcmpfi  20292  flimsncls  20465  tmdgsum  20572  tsmsgsum  20615  tsmsgsumOLD  20618  imasdsf1olem  20854  reconnlem1  21309  fsumcn  21352  ovolfiniun  21890  volfiniun  21935  ovolioo  21956  mbfconstlem  22014  i1fima2  22064  i1fd  22066  itg1val2  22069  itgfsum  22211  itgsplitioo  22222  dvmptfsum  22354  lhop1lem  22392  lhop  22395  vieta1lem2  22685  chtprm  23405  perfectlem2  23483  usgrares1  24388  nbgrassvwo  24415  nbgrassvwo2  24416  2pthlem2  24576  eupap1  24954  eupath2lem3  24957  vdegp1ai  24962  vdegp1bi  24963  ex-dif  25122  ex-in  25124  ofpreima2  27486  eulerpartlemt  28288  eulerpartgbij  28289  ballotlemfp1  28408  subfacp1lem5  28606  cvmliftlem4  28711  cvmliftlem5  28712  mrsubvrs  28860  wfrlem13  29331  finixpnum  30014  mapfzcons2  30627  jm2.23  30914  kelac2lem  30986  kelac2  30987  pwslnm  31016  arearect  31159  fsumsplitsn  31525  fprodsplitsn  31546  volioc  31725  fsumsplitsndif  32300  bnj1421  33966  bj-disjcsn  34388  bj-xpimasn  34395  bj-xpima1snALT  34397