Theorem disjsn 4650

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 4387	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 360	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4578	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 350	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 400	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 298	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1788	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2816	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 336	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 298	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ∩ cin 3889  ∅c0 4268  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-dif 3893  df-in 3897  df-nul 4269  df-sn 4563

This theorem is referenced by:  disjsn2  4651  ssdifsn  4728  ssunsn2  4765  opwo0id  5445  ndmima  6062  xpimasn  6143  snres0  6256  orddisj  6355  fnunop  6608  ressnop0  7103  ftpg  7106  funressn  7109  fsnunf  7136  fsnunfv  7138  frxp2  8091  frxp3  8098  frrlem11  8243  frrlem12  8244  domdifsn  8995  domunsncan  9012  map2xp  9082  limensuci  9088  infensuc  9090  dif1enlem  9091  unfi  9102  ssfi  9104  php  9138  isinf  9172  ac6sfi  9191  fodomfi  9219  fodomfiOLD  9237  funsnfsupp  9302  disjcsn  9522  infdifsn  9576  cantnfp1lem3  9599  pm54.43  9923  dif1card  9930  numacn  9969  kmlem2  10072  dju1en  10092  ackbij1lem1  10139  ackbij1lem18  10156  fin23lem26  10245  isfin1-3  10306  axdc3lem4  10373  unsnen  10473  fpwwe2lem12  10563  ssxr  11213  fzpreddisj  13525  fzp1disj  13535  prinfzo0  13651  fzennn  13928  hashunsng  14352  hashunsngx  14353  hashxplem  14393  hashmap  14395  hashbclem  14412  hashf1lem1  14415  fsumsplitsn  15704  sumtp  15709  fsumsplitsnun  15715  fsum2dlem  15730  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  isumltss  15811  fprodm1  15930  fprod2dlem  15943  fprodsplitsn  15952  fprodfvdvdsd  16301  bitsinv1  16409  bitsinvp1  16416  vdwmc2  16948  prmdvdsprmo  17011  structcnvcnv  17121  f1omvdco3  19422  psgnunilem5  19467  gsumzunsnd  19929  gsumunsnfd  19930  gsum2dlem2  19944  dprd2da  20017  ablfac1eulem  20047  ablfac1eu  20048  fidomndrng  20752  lbsextlem4  21161  cnfldfun  21368  mplmonmul  22019  psrbag0  22045  ist1-2  23337  locfindis  23520  xkohaus  23643  ptcmpfi  23803  flimsncls  23976  tmdgsum  24085  tsmsgsum  24129  imasdsf1olem  24363  reconnlem1  24817  fsumcn  24862  ovolfiniun  25493  volfiniun  25539  ovolioo  25560  mbfconstlem  25619  i1fima2  25671  i1fd  25673  itg1val2  25676  itgfsum  25819  itgsplitioo  25830  dvmptfsum  25967  lhop1lem  26005  lhop  26008  vieta1lem2  26302  chtprm  27141  perfectlem2  27218  noextend  27655  noextenddif  27657  noextendlt  27658  noextendgt  27659  nosupbnd2lem1  27704  nbgrssvwo2  29456  p1evtxdeqlem  29606  eupthp1  30311  eupth2eucrct  30312  trlsegvdeg  30322  ex-dif  30518  ex-in  30520  ex-hash  30548  pliguhgr  30582  ofpreima2  32765  padct  32817  fzdif2  32889  fzodif2  32890  cycpmco2f1  33212  elrgspnlem4  33333  elrspunsn  33519  mplidomlem  33718  psrmonmul  33741  vieta  33771  lindsunlem  33815  esumrnmpt2  34259  esum2dlem  34283  carsgclctunlem1  34508  eulerpartlemt  34562  eulerpartgbij  34563  ballotlemfp1  34683  actfunsnf1o  34795  actfunsnrndisj  34796  chtvalz  34820  bnj1421  35231  f1resfz0f1d  35349  subfacp1lem5  35419  cvmliftlem4  35523  cvmliftlem5  35524  mrsubvrs  35757  dfttc4lem2  36764  bj-xpimasn  37315  bj-xpima1snALT  37317  finixpnum  37979  poimirlem3  37997  poimirlem4  37998  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem27  38021  dvrelog2  42556  dvrelog3  42557  mapfzcons2  43175  jm2.23  43448  kelac2lem  43516  kelac2  43517  pwslnm  43546  arearect  43667  iunrelexp0  44153  gneispace  44585  disjiun2  45513  mpct  45654  volioc  46422  volico  46433  sge0iunmptlemfi  46863  sge0splitsn  46891  ismeannd  46917  fsumsplitsndif  47851  perfectALTVlem2  48220  resinsn  49369  resinsnALT  49370  tposrescnv  49376  tposres3  49378