Theorem disjsn 4644

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 4381	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4574	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 296	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1823	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1785	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2818	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 334	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 296	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ∩ cin 3882  ∅c0 4253  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-dif 3886  df-in 3890  df-nul 4254  df-sn 4559

This theorem is referenced by:  disjsn2  4645  ssdifsn  4718  ssunsn2  4757  opwo0id  5405  ndmima  6000  xpimasn  6077  orddisj  6289  fnunop  6531  ressnop0  7007  ftpg  7010  funressn  7013  fsnunf  7039  fsnunfv  7041  frrlem11  8083  frrlem12  8084  wfrlem13OLD  8123  enpr2d  8792  domdifsn  8795  domunsncan  8812  map2xp  8883  limensuci  8889  infensuc  8891  php  8897  dif1enlem  8905  unfi  8917  ssfi  8918  isinf  8965  ac6sfi  8988  fodomfi  9022  funsnfsupp  9082  infdifsn  9345  cantnfp1lem3  9368  pm54.43  9690  dif1card  9697  numacn  9736  kmlem2  9838  dju1en  9858  ackbij1lem1  9907  ackbij1lem18  9924  fin23lem26  10012  isfin1-3  10073  axdc3lem4  10140  unsnen  10240  fpwwe2lem12  10329  ssxr  10975  fzpreddisj  13234  fzp1disj  13244  prinfzo0  13354  fzennn  13616  hashunsng  14035  hashunsngx  14036  hashxplem  14076  hashmap  14078  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  fsumsplitsn  15384  sumtp  15389  fsumsplitsnun  15395  fsum2dlem  15410  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  isumltss  15488  fprodm1  15605  fprod2dlem  15618  fprodsplitsn  15627  fprodfvdvdsd  15971  bitsinv1  16077  bitsinvp1  16084  vdwmc2  16608  prmdvdsprmo  16671  structcnvcnv  16782  f1omvdco3  18972  psgnunilem5  19017  gsumzunsnd  19472  gsumunsnfd  19473  gsum2dlem2  19487  dprd2da  19560  ablfac1eulem  19590  ablfac1eu  19591  lbsextlem4  20338  fidomndrng  20492  cnfldfunALT  20523  mplmonmul  21147  psrbag0  21180  ist1-2  22406  locfindis  22589  xkohaus  22712  ptcmpfi  22872  flimsncls  23045  tmdgsum  23154  tsmsgsum  23198  imasdsf1olem  23434  reconnlem1  23895  fsumcn  23939  ovolfiniun  24570  volfiniun  24616  ovolioo  24637  mbfconstlem  24696  i1fima2  24748  i1fd  24750  itg1val2  24753  itgfsum  24896  itgsplitioo  24907  dvmptfsum  25044  lhop1lem  25082  lhop  25085  vieta1lem2  25376  chtprm  26207  perfectlem2  26283  nbgrssvwo2  27632  p1evtxdeqlem  27782  eupthp1  28481  eupth2eucrct  28482  trlsegvdeg  28492  ex-dif  28688  ex-in  28690  ex-hash  28718  pliguhgr  28749  ofpreima2  30905  padct  30956  fzdif2  31014  fzodif2  31015  cycpmco2f1  31293  lindsunlem  31607  esumrnmpt2  31936  esum2dlem  31960  carsgclctunlem1  32184  eulerpartlemt  32238  eulerpartgbij  32239  ballotlemfp1  32358  actfunsnf1o  32484  actfunsnrndisj  32485  chtvalz  32509  bnj1421  32922  f1resfz0f1d  32972  subfacp1lem5  33046  cvmliftlem4  33150  cvmliftlem5  33151  mrsubvrs  33384  snres0  33577  frxp2  33718  frxp3  33724  noextend  33796  noextenddif  33798  noextendlt  33799  noextendgt  33800  nosupbnd2lem1  33845  bj-disjcsn  35068  bj-xpimasn  35072  bj-xpima1snALT  35074  finixpnum  35689  poimirlem3  35707  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem27  35731  dvrelog2  40000  dvrelog3  40001  mapfzcons2  40457  jm2.23  40734  kelac2lem  40805  kelac2  40806  pwslnm  40835  arearect  40962  iunrelexp0  41199  gneispace  41633  disjiun2  42495  mpct  42630  volioc  43403  volico  43414  sge0iunmptlemfi  43841  sge0splitsn  43869  ismeannd  43895  fsumsplitsndif  44713  perfectALTVlem2  45062