Theorem disjsn 4613

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 4351	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 363	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4543	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 353	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 403	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1827	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1789	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2810	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 300	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ∩ cin 3852  ∅c0 4223  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-v 3400  df-dif 3856  df-in 3860  df-nul 4224  df-sn 4528

This theorem is referenced by:  disjsn2  4614  ssdifsn  4687  ssunsn2  4726  opwo0id  5365  ndmima  5951  xpimasn  6028  orddisj  6229  fnunop  6470  ressnop0  6946  ftpg  6949  funressn  6952  fsnunf  6978  fsnunfv  6980  frrlem11  8015  frrlem12  8016  wfrlem13  8045  enpr2d  8703  domdifsn  8706  domunsncan  8723  map2xp  8794  limensuci  8800  infensuc  8802  php  8808  dif1enlem  8816  unfi  8828  ssfi  8829  isinf  8867  ac6sfi  8893  fodomfi  8927  funsnfsupp  8987  infdifsn  9250  cantnfp1lem3  9273  pm54.43  9582  dif1card  9589  numacn  9628  kmlem2  9730  dju1en  9750  ackbij1lem1  9799  ackbij1lem18  9816  fin23lem26  9904  isfin1-3  9965  axdc3lem4  10032  unsnen  10132  fpwwe2lem12  10221  ssxr  10867  fzpreddisj  13126  fzp1disj  13136  prinfzo0  13246  fzennn  13506  hashunsng  13924  hashunsngx  13925  hashxplem  13965  hashmap  13967  hashbclem  13981  hashf1lem1  13985  hashf1lem1OLD  13986  fsumsplitsn  15272  sumtp  15276  fsumsplitsnun  15282  fsum2dlem  15297  fsumabs  15328  fsumrlim  15338  fsumo1  15339  fsumiun  15348  isumltss  15375  fprodm1  15492  fprod2dlem  15505  fprodsplitsn  15514  fprodfvdvdsd  15858  bitsinv1  15964  bitsinvp1  15971  vdwmc2  16495  prmdvdsprmo  16558  structcnvcnv  16680  f1omvdco3  18795  psgnunilem5  18840  gsumzunsnd  19295  gsumunsnfd  19296  gsum2dlem2  19310  dprd2da  19383  ablfac1eulem  19413  ablfac1eu  19414  lbsextlem4  20152  fidomndrng  20299  cnfldfunALT  20330  mplmonmul  20947  psrbag0  20974  ist1-2  22198  locfindis  22381  xkohaus  22504  ptcmpfi  22664  flimsncls  22837  tmdgsum  22946  tsmsgsum  22990  imasdsf1olem  23225  reconnlem1  23677  fsumcn  23721  ovolfiniun  24352  volfiniun  24398  ovolioo  24419  mbfconstlem  24478  i1fima2  24530  i1fd  24532  itg1val2  24535  itgfsum  24678  itgsplitioo  24689  dvmptfsum  24826  lhop1lem  24864  lhop  24867  vieta1lem2  25158  chtprm  25989  perfectlem2  26065  nbgrssvwo2  27404  p1evtxdeqlem  27554  eupthp1  28253  eupth2eucrct  28254  trlsegvdeg  28264  ex-dif  28460  ex-in  28462  ex-hash  28490  pliguhgr  28521  ofpreima2  30677  padct  30728  fzdif2  30786  fzodif2  30787  cycpmco2f1  31064  lindsunlem  31373  esumrnmpt2  31702  esum2dlem  31726  carsgclctunlem1  31950  eulerpartlemt  32004  eulerpartgbij  32005  ballotlemfp1  32124  actfunsnf1o  32250  actfunsnrndisj  32251  chtvalz  32275  bnj1421  32689  f1resfz0f1d  32739  subfacp1lem5  32813  cvmliftlem4  32917  cvmliftlem5  32918  mrsubvrs  33151  snres0  33344  frxp2  33471  frxp3  33477  noextend  33555  noextenddif  33557  noextendlt  33558  noextendgt  33559  nosupbnd2lem1  33604  bj-disjcsn  34827  bj-xpimasn  34831  bj-xpima1snALT  34833  finixpnum  35448  poimirlem3  35466  poimirlem4  35467  poimirlem13  35476  poimirlem14  35477  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem27  35490  dvrelog2  39754  dvrelog3  39755  mapfzcons2  40185  jm2.23  40462  kelac2lem  40533  kelac2  40534  pwslnm  40563  arearect  40690  iunrelexp0  40928  gneispace  41362  disjiun2  42220  mpct  42355  volioc  43131  volico  43142  sge0iunmptlemfi  43569  sge0splitsn  43597  ismeannd  43623  fsumsplitsndif  44441  perfectALTVlem2  44790