Theorem disjsn 4671

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 4411	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4601	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 399	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2804	. . 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 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3910  ∅c0 4292  {csn 4585

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3446  df-dif 3914  df-in 3918  df-nul 4293  df-sn 4586

This theorem is referenced by:  disjsn2  4672  ssdifsn  4748  ssunsn2  4787  opwo0id  5452  ndmima  6063  xpimasn  6146  snres0  6259  orddisj  6358  fnunop  6616  ressnop0  7107  ftpg  7110  funressn  7113  fsnunf  7141  fsnunfv  7143  frxp2  8100  frxp3  8107  frrlem11  8252  frrlem12  8253  enpr2dOLD  8998  domdifsn  9001  domunsncan  9018  map2xp  9088  limensuci  9094  infensuc  9096  dif1enlem  9097  dif1enlemOLD  9098  unfi  9112  ssfi  9114  php  9148  isinf  9183  isinfOLD  9184  ac6sfi  9207  fodomfi  9237  fodomfiOLD  9257  funsnfsupp  9319  disjcsn  9533  infdifsn  9586  cantnfp1lem3  9609  pm54.43  9930  dif1card  9939  numacn  9978  kmlem2  10081  dju1en  10101  ackbij1lem1  10148  ackbij1lem18  10165  fin23lem26  10254  isfin1-3  10315  axdc3lem4  10382  unsnen  10482  fpwwe2lem12  10571  ssxr  11219  fzpreddisj  13510  fzp1disj  13520  prinfzo0  13635  fzennn  13909  hashunsng  14333  hashunsngx  14334  hashxplem  14374  hashmap  14376  hashbclem  14393  hashf1lem1  14396  fsumsplitsn  15686  sumtp  15691  fsumsplitsnun  15697  fsum2dlem  15712  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  isumltss  15790  fprodm1  15909  fprod2dlem  15922  fprodsplitsn  15931  fprodfvdvdsd  16280  bitsinv1  16388  bitsinvp1  16395  vdwmc2  16926  prmdvdsprmo  16989  structcnvcnv  17099  f1omvdco3  19355  psgnunilem5  19400  gsumzunsnd  19862  gsumunsnfd  19863  gsum2dlem2  19877  dprd2da  19950  ablfac1eulem  19980  ablfac1eu  19981  fidomndrng  20658  lbsextlem4  21047  cnfldfun  21254  cnfldfunOLD  21267  mplmonmul  21919  psrbag0  21945  ist1-2  23210  locfindis  23393  xkohaus  23516  ptcmpfi  23676  flimsncls  23849  tmdgsum  23958  tsmsgsum  24002  imasdsf1olem  24237  reconnlem1  24691  fsumcn  24737  ovolfiniun  25378  volfiniun  25424  ovolioo  25445  mbfconstlem  25504  i1fima2  25556  i1fd  25558  itg1val2  25561  itgfsum  25704  itgsplitioo  25715  dvmptfsum  25855  lhop1lem  25894  lhop  25897  vieta1lem2  26195  chtprm  27039  perfectlem2  27117  noextend  27554  noextenddif  27556  noextendlt  27557  noextendgt  27558  nosupbnd2lem1  27603  nbgrssvwo2  29265  p1evtxdeqlem  29416  eupthp1  30118  eupth2eucrct  30119  trlsegvdeg  30129  ex-dif  30325  ex-in  30327  ex-hash  30355  pliguhgr  30388  ofpreima2  32563  padct  32616  fzdif2  32686  fzodif2  32687  cycpmco2f1  33054  elrgspnlem4  33169  elrspunsn  33373  lindsunlem  33593  esumrnmpt2  34031  esum2dlem  34055  carsgclctunlem1  34281  eulerpartlemt  34335  eulerpartgbij  34336  ballotlemfp1  34456  actfunsnf1o  34568  actfunsnrndisj  34569  chtvalz  34593  bnj1421  35005  f1resfz0f1d  35074  subfacp1lem5  35144  cvmliftlem4  35248  cvmliftlem5  35249  mrsubvrs  35482  bj-xpimasn  36916  bj-xpima1snALT  36918  finixpnum  37572  poimirlem3  37590  poimirlem4  37591  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem27  37614  dvrelog2  42025  dvrelog3  42026  mapfzcons2  42680  jm2.23  42958  kelac2lem  43026  kelac2  43027  pwslnm  43056  arearect  43177  iunrelexp0  43664  gneispace  44096  disjiun2  45025  mpct  45168  volioc  45943  volico  45954  sge0iunmptlemfi  46384  sge0splitsn  46412  ismeannd  46438  fsumsplitsndif  47347  perfectALTVlem2  47696  resinsn  48833  resinsnALT  48834  tposrescnv  48840  tposres3  48842