Theorem disjsn 4032

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 3807	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 336	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		elsn 3982	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 327	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 424	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 275	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1691	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1665	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2447	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 313	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 275	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   A.wal 1442   = wceq 1444   E.wex 1663   e. wcel 1887   i^i cin 3403   (/)c0 3731   {csn 3968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047  df-dif 3407  df-in 3411  df-nul 3732  df-sn 3969

This theorem is referenced by:  disjsn2  4033  ssunsn2  4131  ndmima  5205  ndmimaOLD  5206  xpimasn  5282  orddisj  5461  funtpg  5632  fnunsn  5683  ressnop0  6071  ftpg  6074  funressn  6077  fsnunf  6102  fsnunfv  6104  wfrlem13  7048  domdifsn  7655  domunsncan  7672  map2xp  7742  limensuci  7748  infensuc  7750  php  7756  isinf  7785  ac6sfi  7815  fodomfi  7850  funsnfsupp  7907  infdifsn  8162  cantnfp1lem3  8185  pm54.43  8434  dif1card  8441  numacn  8480  kmlem2  8581  cda1en  8605  ackbij1lem1  8650  ackbij1lem18  8667  fin23lem26  8755  isfin1-3  8816  axdc3lem4  8883  unsnen  8978  fpwwe2lem13  9067  ssxr  9703  fzpreddisj  11845  fzp1disj  11854  fzennn  12181  hashunsng  12571  hashxplem  12605  hashmap  12607  hashbclem  12615  hashf1lem1  12618  cats1un  12832  sumtp  13810  fsumsplitsnun  13816  fsum2dlem  13831  fsumabs  13861  fsumrlim  13871  fsumo1  13872  fsumiun  13881  isumltss  13906  fprodm1  14021  fprod2dlem  14034  fprodsplitsn  14043  fproddvdsd  14370  bitsinv1  14416  bitsinvp1  14423  isprm2lem  14631  vdwmc2  14929  prmdvdsprmo  15000  prmdvdsprmorOLD  15015  structcnvcnv  15132  strlemor1  15217  f1omvdco3  17090  psgnunilem5  17135  gsumzaddlem  17554  gsumzunsnd  17588  gsumunsnfd  17589  gsum2dlem2  17603  dprd2da  17675  ablfac1eulem  17705  ablfac1eu  17706  lbsextlem4  18384  fidomndrng  18531  mplmonmul  18688  psrbag0  18717  ist1-2  20363  locfindis  20545  xkohaus  20668  ptcmpfi  20828  flimsncls  21001  tmdgsum  21110  tsmsgsum  21153  imasdsf1olem  21388  reconnlem1  21844  fsumcn  21902  ovolfiniun  22454  volfiniun  22500  ovolioo  22521  mbfconstlem  22585  i1fima2  22637  i1fd  22639  itg1val2  22642  itgfsum  22784  itgsplitioo  22795  dvmptfsum  22927  lhop1lem  22965  lhop  22968  vieta1lem2  23264  chtprm  24080  perfectlem2  24158  usgrares1  25138  nbgrassvwo  25165  nbgrassvwo2  25166  2pthlem2  25326  eupap1  25704  eupath2lem3  25707  vdegp1ai  25712  vdegp1bi  25713  ex-dif  25873  ex-in  25875  ofpreima2  28269  padct  28307  fzdif2  28369  esumrnmpt2  28889  esum2dlem  28913  carsgclctunlem1  29149  eulerpartlemt  29204  eulerpartgbij  29205  ballotlemfp1  29324  bnj1421  29851  subfacp1lem5  29907  cvmliftlem4  30011  cvmliftlem5  30012  mrsubvrs  30160  bj-disjcsn  31542  bj-xpimasn  31548  bj-xpima1snALT  31550  finixpnum  31930  poimirlem3  31943  poimirlem4  31944  poimirlem13  31953  poimirlem14  31954  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem18  31958  poimirlem19  31959  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem27  31967  mapfzcons2  35561  jm2.23  35851  kelac2lem  35922  kelac2  35923  pwslnm  35952  arearect  36100  iunrelexp0  36294  disjiun2  37398  mpct  37482  fsumsplitsn  37649  volioc  37849  sge0iunmptlemfi  38255  sge0splitsn  38283  ismeannd  38305  volico  38363  perfectALTVlem2  38844  prinfzo0  39066  fsumsplitsndif  39092  nbgrssvwo2  39433