Theorem disjsn 4655

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 4392	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4583	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2812	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 297	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3888  ∅c0 4273  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-dif 3892  df-in 3896  df-nul 4274  df-sn 4568

This theorem is referenced by:  disjsn2  4656  ssdifsn  4733  ssunsn2  4770  opwo0id  5451  ndmima  6068  xpimasn  6149  snres0  6262  orddisj  6361  fnunop  6614  ressnop0  7107  ftpg  7110  funressn  7113  fsnunf  7140  fsnunfv  7142  frxp2  8094  frxp3  8101  frrlem11  8246  frrlem12  8247  domdifsn  8998  domunsncan  9015  map2xp  9085  limensuci  9091  infensuc  9093  dif1enlem  9094  unfi  9105  ssfi  9107  php  9141  isinf  9175  ac6sfi  9194  fodomfi  9222  fodomfiOLD  9240  funsnfsupp  9305  disjcsn  9524  infdifsn  9578  cantnfp1lem3  9601  pm54.43  9925  dif1card  9932  numacn  9971  kmlem2  10074  dju1en  10094  ackbij1lem1  10141  ackbij1lem18  10158  fin23lem26  10247  isfin1-3  10308  axdc3lem4  10375  unsnen  10475  fpwwe2lem12  10565  ssxr  11215  fzpreddisj  13527  fzp1disj  13537  prinfzo0  13653  fzennn  13930  hashunsng  14354  hashunsngx  14355  hashxplem  14395  hashmap  14397  hashbclem  14414  hashf1lem1  14417  fsumsplitsn  15706  sumtp  15711  fsumsplitsnun  15717  fsum2dlem  15732  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  isumltss  15813  fprodm1  15932  fprod2dlem  15945  fprodsplitsn  15954  fprodfvdvdsd  16303  bitsinv1  16411  bitsinvp1  16418  vdwmc2  16950  prmdvdsprmo  17013  structcnvcnv  17123  f1omvdco3  19424  psgnunilem5  19469  gsumzunsnd  19931  gsumunsnfd  19932  gsum2dlem2  19946  dprd2da  20019  ablfac1eulem  20049  ablfac1eu  20050  fidomndrng  20750  lbsextlem4  21159  cnfldfun  21366  mplmonmul  22014  psrbag0  22040  ist1-2  23312  locfindis  23495  xkohaus  23618  ptcmpfi  23778  flimsncls  23951  tmdgsum  24060  tsmsgsum  24104  imasdsf1olem  24338  reconnlem1  24792  fsumcn  24837  ovolfiniun  25468  volfiniun  25514  ovolioo  25535  mbfconstlem  25594  i1fima2  25646  i1fd  25648  itg1val2  25651  itgfsum  25794  itgsplitioo  25805  dvmptfsum  25942  lhop1lem  25980  lhop  25983  vieta1lem2  26277  chtprm  27116  perfectlem2  27193  noextend  27630  noextenddif  27632  noextendlt  27633  noextendgt  27634  nosupbnd2lem1  27679  nbgrssvwo2  29431  p1evtxdeqlem  29581  eupthp1  30286  eupth2eucrct  30287  trlsegvdeg  30297  ex-dif  30493  ex-in  30495  ex-hash  30523  pliguhgr  30557  ofpreima2  32739  padct  32791  fzdif2  32863  fzodif2  32864  cycpmco2f1  33185  elrgspnlem4  33306  elrspunsn  33489  psrmonmul  33694  vieta  33724  lindsunlem  33768  esumrnmpt2  34212  esum2dlem  34236  carsgclctunlem1  34461  eulerpartlemt  34515  eulerpartgbij  34516  ballotlemfp1  34636  actfunsnf1o  34748  actfunsnrndisj  34749  chtvalz  34773  bnj1421  35184  f1resfz0f1d  35296  subfacp1lem5  35366  cvmliftlem4  35470  cvmliftlem5  35471  mrsubvrs  35704  dfttc4lem2  36711  bj-xpimasn  37262  bj-xpima1snALT  37264  finixpnum  37926  poimirlem3  37944  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem27  37968  dvrelog2  42503  dvrelog3  42504  mapfzcons2  43151  jm2.23  43424  kelac2lem  43492  kelac2  43493  pwslnm  43522  arearect  43643  iunrelexp0  44129  gneispace  44561  disjiun2  45489  mpct  45630  volioc  46400  volico  46411  sge0iunmptlemfi  46841  sge0splitsn  46869  ismeannd  46895  fsumsplitsndif  47829  perfectALTVlem2  48198  resinsn  49347  resinsnALT  49348  tposrescnv  49354  tposres3  49356