Theorem disjsn 4640

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 4394	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 362	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4576	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 402	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 299	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2893	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 337	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 299	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ∩ cin 3928  ∅c0 4284  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ral 3142  df-v 3493  df-dif 3932  df-in 3936  df-nul 4285  df-sn 4561

This theorem is referenced by:  disjsn2  4641  ssdifsn  4713  ssunsn2  4753  opwo0id  5380  ndmima  5959  xpimasn  6035  orddisj  6222  fnunsn  6457  ressnop0  6908  ftpg  6911  funressn  6914  fsnunf  6940  fsnunfv  6942  wfrlem13  7960  enpr2d  8590  domdifsn  8593  domunsncan  8610  map2xp  8680  limensuci  8686  infensuc  8688  php  8694  isinf  8724  ac6sfi  8755  fodomfi  8790  funsnfsupp  8850  infdifsn  9113  cantnfp1lem3  9136  pm54.43  9422  dif1card  9429  numacn  9468  kmlem2  9570  dju1en  9590  ackbij1lem1  9635  ackbij1lem18  9652  fin23lem26  9740  isfin1-3  9801  axdc3lem4  9868  unsnen  9968  fpwwe2lem13  10057  ssxr  10703  fzpreddisj  12953  fzp1disj  12963  prinfzo0  13073  fzennn  13333  hashunsng  13750  hashunsngx  13751  hashxplem  13791  hashmap  13793  hashbclem  13807  hashf1lem1  13810  fsumsplitsn  15095  sumtp  15099  fsumsplitsnun  15105  fsum2dlem  15120  fsumabs  15151  fsumrlim  15161  fsumo1  15162  fsumiun  15171  isumltss  15198  fprodm1  15316  fprod2dlem  15329  fprodsplitsn  15338  fprodfvdvdsd  15678  bitsinv1  15786  bitsinvp1  15793  vdwmc2  16310  prmdvdsprmo  16373  structcnvcnv  16492  f1omvdco3  18572  psgnunilem5  18617  gsumzunsnd  19071  gsumunsnfd  19072  gsum2dlem2  19086  dprd2da  19159  ablfac1eulem  19189  ablfac1eu  19190  lbsextlem4  19928  fidomndrng  20075  mplmonmul  20240  psrbag0  20269  cnfldfunALT  20553  ist1-2  21950  locfindis  22133  xkohaus  22256  ptcmpfi  22416  flimsncls  22589  tmdgsum  22698  tsmsgsum  22742  imasdsf1olem  22978  reconnlem1  23429  fsumcn  23473  ovolfiniun  24097  volfiniun  24143  ovolioo  24164  mbfconstlem  24223  i1fima2  24275  i1fd  24277  itg1val2  24280  itgfsum  24422  itgsplitioo  24433  dvmptfsum  24569  lhop1lem  24607  lhop  24610  vieta1lem2  24898  chtprm  25728  perfectlem2  25804  nbgrssvwo2  27142  p1evtxdeqlem  27292  eupthp1  27993  eupth2eucrct  27994  trlsegvdeg  28004  ex-dif  28200  ex-in  28202  ex-hash  28230  pliguhgr  28261  ofpreima2  30411  padct  30455  fzdif2  30514  fzodif2  30515  cycpmco2f1  30787  lindsunlem  31044  esumrnmpt2  31348  esum2dlem  31372  carsgclctunlem1  31596  eulerpartlemt  31650  eulerpartgbij  31651  ballotlemfp1  31770  actfunsnf1o  31896  actfunsnrndisj  31897  chtvalz  31921  bnj1421  32335  f1resfz0f1d  32382  subfacp1lem5  32452  cvmliftlem4  32556  cvmliftlem5  32557  mrsubvrs  32790  frrlem11  33154  frrlem12  33155  noextend  33194  noextenddif  33196  noextendlt  33197  noextendgt  33198  nosupbnd2lem1  33236  bj-disjcsn  34287  bj-xpimasn  34291  bj-xpima1snALT  34293  finixpnum  34912  poimirlem3  34930  poimirlem4  34931  poimirlem13  34940  poimirlem14  34941  poimirlem15  34942  poimirlem16  34943  poimirlem17  34944  poimirlem18  34945  poimirlem19  34946  poimirlem20  34947  poimirlem21  34948  poimirlem22  34949  poimirlem27  34954  dffltz  39347  mapfzcons2  39392  jm2.23  39669  kelac2lem  39740  kelac2  39741  pwslnm  39770  arearect  39897  iunrelexp0  40121  gneispace  40558  disjiun2  41394  mpct  41538  volioc  42331  volico  42342  sge0iunmptlemfi  42769  sge0splitsn  42797  ismeannd  42823  fsumsplitsndif  43607  perfectALTVlem2  43961