Theorem disjsn 4246

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 4019	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 349	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 4193	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 339	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 438	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 286	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1747	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1706	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2618	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 325	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 286	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   i^i cin 3573   (/)c0 3915   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916  df-sn 4178

This theorem is referenced by:  disjsn2  4247  ssunsn2  4359  opwo0id  4961  ndmima  5502  xpimasn  5579  orddisj  5762  funtpgOLD  5943  fnunsn  5998  ressnop0  6420  ftpg  6423  funressn  6426  fsnunf  6451  fsnunfv  6453  wfrlem13  7427  domdifsn  8043  domunsncan  8060  map2xp  8130  limensuci  8136  infensuc  8138  php  8144  isinf  8173  ac6sfi  8204  fodomfi  8239  funsnfsupp  8299  infdifsn  8554  cantnfp1lem3  8577  pm54.43  8826  dif1card  8833  numacn  8872  kmlem2  8973  cda1en  8997  ackbij1lem1  9042  ackbij1lem18  9059  fin23lem26  9147  isfin1-3  9208  axdc3lem4  9275  unsnen  9375  fpwwe2lem13  9464  ssxr  10107  fzpreddisj  12390  fzp1disj  12399  prinfzo0  12506  fzennn  12767  hashunsng  13181  hashxplem  13220  hashmap  13222  hashbclem  13236  hashf1lem1  13239  cats1un  13475  fsumsplitsn  14474  sumtp  14478  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  fsum2dlem  14501  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  isumltss  14580  fprodm1  14697  fprod2dlem  14710  fprodsplitsn  14720  fprodfvdvdsd  15058  bitsinv1  15164  bitsinvp1  15171  vdwmc2  15683  prmdvdsprmo  15746  structcnvcnv  15871  strlemor1OLD  15969  f1omvdco3  17869  psgnunilem5  17914  gsumzunsnd  18355  gsumunsnfd  18356  gsum2dlem2  18370  dprd2da  18441  ablfac1eulem  18471  ablfac1eu  18472  lbsextlem4  19161  fidomndrng  19307  mplmonmul  19464  psrbag0  19494  cnfldfunALT  19759  ist1-2  21151  locfindis  21333  xkohaus  21456  ptcmpfi  21616  flimsncls  21790  tmdgsum  21899  tsmsgsum  21942  imasdsf1olem  22178  reconnlem1  22629  fsumcn  22673  ovolfiniun  23269  volfiniun  23315  ovolioo  23336  mbfconstlem  23396  i1fima2  23446  i1fd  23448  itg1val2  23451  itgfsum  23593  itgsplitioo  23604  dvmptfsum  23738  lhop1lem  23776  lhop  23779  vieta1lem2  24066  chtprm  24879  perfectlem2  24955  nbgrssvwo2  26261  p1evtxdeqlem  26408  eupthp1  27076  eupth2eucrct  27077  trlsegvdeg  27087  ex-dif  27280  ex-in  27282  ex-hash  27310  pliguhgr  27338  ofpreima2  29466  padct  29497  fzdif2  29551  fzodif2  29552  esumrnmpt2  30130  esum2dlem  30154  carsgclctunlem1  30379  eulerpartlemt  30433  eulerpartgbij  30434  ballotlemfp1  30553  actfunsnf1o  30682  actfunsnrndisj  30683  chtvalz  30707  bnj1421  31110  subfacp1lem5  31166  cvmliftlem4  31270  cvmliftlem5  31271  mrsubvrs  31419  noextend  31819  noextenddif  31821  noextendlt  31822  noextendgt  31823  nosupbnd2lem1  31861  bj-disjcsn  32936  bj-xpimasn  32942  bj-xpima1snALT  32944  finixpnum  33394  poimirlem3  33412  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem27  33436  mapfzcons2  37282  jm2.23  37563  kelac2lem  37634  kelac2  37635  pwslnm  37664  arearect  37801  iunrelexp0  37994  gneispace  38432  disjiun2  39226  mpct  39393  volioc  40188  volico  40200  sge0iunmptlemfi  40630  sge0splitsn  40658  ismeannd  40684  fsumsplitsndif  41343  perfectALTVlem2  41631