Theorem disjsn 4656

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 4393	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4584	. . . . 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 2813	. . 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 3889  ∅c0 4274  {csn 4568

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275  df-sn 4569

This theorem is referenced by:  disjsn2  4657  ssdifsn  4732  ssunsn2  4771  opwo0id  5445  ndmima  6062  xpimasn  6143  snres0  6256  orddisj  6355  fnunop  6608  ressnop0  7100  ftpg  7103  funressn  7106  fsnunf  7133  fsnunfv  7135  frxp2  8087  frxp3  8094  frrlem11  8239  frrlem12  8240  domdifsn  8991  domunsncan  9008  map2xp  9078  limensuci  9084  infensuc  9086  dif1enlem  9087  unfi  9098  ssfi  9100  php  9134  isinf  9168  ac6sfi  9187  fodomfi  9215  fodomfiOLD  9233  funsnfsupp  9298  disjcsn  9515  infdifsn  9569  cantnfp1lem3  9592  pm54.43  9916  dif1card  9923  numacn  9962  kmlem2  10065  dju1en  10085  ackbij1lem1  10132  ackbij1lem18  10149  fin23lem26  10238  isfin1-3  10299  axdc3lem4  10366  unsnen  10466  fpwwe2lem12  10556  ssxr  11206  fzpreddisj  13518  fzp1disj  13528  prinfzo0  13644  fzennn  13921  hashunsng  14345  hashunsngx  14346  hashxplem  14386  hashmap  14388  hashbclem  14405  hashf1lem1  14408  fsumsplitsn  15697  sumtp  15702  fsumsplitsnun  15708  fsum2dlem  15723  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  isumltss  15804  fprodm1  15923  fprod2dlem  15936  fprodsplitsn  15945  fprodfvdvdsd  16294  bitsinv1  16402  bitsinvp1  16409  vdwmc2  16941  prmdvdsprmo  17004  structcnvcnv  17114  f1omvdco3  19415  psgnunilem5  19460  gsumzunsnd  19922  gsumunsnfd  19923  gsum2dlem2  19937  dprd2da  20010  ablfac1eulem  20040  ablfac1eu  20041  fidomndrng  20741  lbsextlem4  21151  cnfldfun  21358  cnfldfunOLD  21371  mplmonmul  22024  psrbag0  22050  ist1-2  23322  locfindis  23505  xkohaus  23628  ptcmpfi  23788  flimsncls  23961  tmdgsum  24070  tsmsgsum  24114  imasdsf1olem  24348  reconnlem1  24802  fsumcn  24847  ovolfiniun  25478  volfiniun  25524  ovolioo  25545  mbfconstlem  25604  i1fima2  25656  i1fd  25658  itg1val2  25661  itgfsum  25804  itgsplitioo  25815  dvmptfsum  25952  lhop1lem  25990  lhop  25993  vieta1lem2  26288  chtprm  27130  perfectlem2  27207  noextend  27644  noextenddif  27646  noextendlt  27647  noextendgt  27648  nosupbnd2lem1  27693  nbgrssvwo2  29445  p1evtxdeqlem  29596  eupthp1  30301  eupth2eucrct  30302  trlsegvdeg  30312  ex-dif  30508  ex-in  30510  ex-hash  30538  pliguhgr  30572  ofpreima2  32754  padct  32806  fzdif2  32878  fzodif2  32879  cycpmco2f1  33200  elrgspnlem4  33321  elrspunsn  33504  psrmonmul  33709  vieta  33739  lindsunlem  33784  esumrnmpt2  34228  esum2dlem  34252  carsgclctunlem1  34477  eulerpartlemt  34531  eulerpartgbij  34532  ballotlemfp1  34652  actfunsnf1o  34764  actfunsnrndisj  34765  chtvalz  34789  bnj1421  35200  f1resfz0f1d  35312  subfacp1lem5  35382  cvmliftlem4  35486  cvmliftlem5  35487  mrsubvrs  35720  dfttc4lem2  36727  bj-xpimasn  37278  bj-xpima1snALT  37280  finixpnum  37940  poimirlem3  37958  poimirlem4  37959  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem27  37982  dvrelog2  42517  dvrelog3  42518  mapfzcons2  43165  jm2.23  43442  kelac2lem  43510  kelac2  43511  pwslnm  43540  arearect  43661  iunrelexp0  44147  gneispace  44579  disjiun2  45507  mpct  45648  volioc  46418  volico  46429  sge0iunmptlemfi  46859  sge0splitsn  46887  ismeannd  46913  fsumsplitsndif  47841  perfectALTVlem2  48210  resinsn  49359  resinsnALT  49360  tposrescnv  49366  tposres3  49368