Theorem disjsn 4192

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	⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Proof of Theorem disjsn

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		disj1 3971	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 348	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4141	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 338	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 437	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 285	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1737	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1697	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		df-clel 2606	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 324	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 285	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ∩ cin 3539  ∅c0 3874  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-dif 3543  df-in 3547  df-nul 3875  df-sn 4126

This theorem is referenced by:  disjsn2  4193  ssunsn2  4299  ndmima  5421  xpimasn  5498  orddisj  5679  funtpgOLD  5857  fnunsn  5912  ressnop0  6325  ftpg  6328  funressn  6331  fsnunf  6356  fsnunfv  6358  wfrlem13  7314  domdifsn  7928  domunsncan  7945  map2xp  8015  limensuci  8021  infensuc  8023  php  8029  isinf  8058  ac6sfi  8089  fodomfi  8124  funsnfsupp  8182  infdifsn  8437  cantnfp1lem3  8460  pm54.43  8709  dif1card  8716  numacn  8755  kmlem2  8856  cda1en  8880  ackbij1lem1  8925  ackbij1lem18  8942  fin23lem26  9030  isfin1-3  9091  axdc3lem4  9158  unsnen  9254  fpwwe2lem13  9343  ssxr  9986  fzpreddisj  12260  fzp1disj  12269  fzennn  12629  hashunsng  13042  hashxplem  13080  hashmap  13082  hashbclem  13093  hashf1lem1  13096  fundmge2nop0  13129  cats1un  13327  sumtp  14322  fsumsplitsnun  14328  fsum2dlem  14343  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  isumltss  14419  fprodm1  14536  fprod2dlem  14549  fprodsplitsn  14559  fprodfvdvdsd  14896  bitsinv1  15002  bitsinvp1  15009  isprm2lem  15232  vdwmc2  15521  prmdvdsprmo  15584  structcnvcnv  15706  strlemor1  15796  f1omvdco3  17692  psgnunilem5  17737  gsumzunsnd  18178  gsumunsnfd  18179  gsum2dlem2  18193  dprd2da  18264  ablfac1eulem  18294  ablfac1eu  18295  lbsextlem4  18982  fidomndrng  19128  mplmonmul  19285  psrbag0  19315  ist1-2  20961  locfindis  21143  xkohaus  21266  ptcmpfi  21426  flimsncls  21600  tmdgsum  21709  tsmsgsum  21752  imasdsf1olem  21988  reconnlem1  22437  fsumcn  22481  ovolfiniun  23076  volfiniun  23122  ovolioo  23143  mbfconstlem  23202  i1fima2  23252  i1fd  23254  itg1val2  23257  itgfsum  23399  itgsplitioo  23410  dvmptfsum  23542  lhop1lem  23580  lhop  23583  vieta1lem2  23870  chtprm  24679  perfectlem2  24755  usgrares1  25939  nbgrassvwo  25966  nbgrassvwo2  25967  2pthlem2  26126  eupap1  26503  eupath2lem3  26506  vdegp1ai  26511  vdegp1bi  26512  ex-dif  26672  ex-in  26674  ex-hash  26702  ofpreima2  28849  padct  28885  fzdif2  28939  esumrnmpt2  29457  esum2dlem  29481  carsgclctunlem1  29706  eulerpartlemt  29760  eulerpartgbij  29761  ballotlemfp1  29880  bnj1421  30364  subfacp1lem5  30420  cvmliftlem4  30524  cvmliftlem5  30525  mrsubvrs  30673  bj-disjcsn  32129  bj-xpimasn  32135  bj-xpima1snALT  32137  finixpnum  32564  poimirlem3  32582  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem27  32606  mapfzcons2  36300  jm2.23  36581  kelac2lem  36652  kelac2  36653  pwslnm  36682  arearect  36820  iunrelexp0  37013  gneispace  37452  disjiun2  38251  mpct  38388  fsumsplitsn  38637  volioc  38864  volico  38876  sge0iunmptlemfi  39306  sge0splitsn  39334  ismeannd  39360  perfectALTVlem2  40165  prinfzo0  40363  fsumsplitsndif  40372  nbgrssvwo2  40587  p1evtxdeqlem  40728  eupthp1  41384  eupth2eucrct  41385  trlsegvdeg  41395