Theorem disjsn 4716

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 4451	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 360	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4645	. . . . 5 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
4	3	imbi1i 350	. . . 4 ⊢ ((𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴))
5		imnan 401	. . . 4 ⊢ ((𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
6	2, 4, 5	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
7	6	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
8		alnex 1784	. . 3 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
9		dfclel 2812	. . 3 ⊢ (𝐵 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴))
10	8, 9	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ ¬ 𝐵 ∈ 𝐴)
11	1, 7, 10	3bitri 297	1 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ∩ cin 3948  ∅c0 4323  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-dif 3952  df-in 3956  df-nul 4324  df-sn 4630

This theorem is referenced by:  disjsn2  4717  ssdifsn  4792  ssunsn2  4831  opwo0id  5498  ndmima  6103  xpimasn  6185  snres0  6298  orddisj  6403  fnunop  6666  ressnop0  7151  ftpg  7154  funressn  7157  fsnunf  7183  fsnunfv  7185  frxp2  8130  frxp3  8137  frrlem11  8281  frrlem12  8282  wfrlem13OLD  8321  enpr2dOLD  9050  domdifsn  9054  domunsncan  9072  map2xp  9147  limensuci  9153  infensuc  9155  dif1enlem  9156  dif1enlemOLD  9157  unfi  9172  ssfi  9173  php  9210  phpOLD  9222  isinf  9260  isinfOLD  9261  ac6sfi  9287  fodomfi  9325  funsnfsupp  9387  disjcsn  9599  infdifsn  9652  cantnfp1lem3  9675  pm54.43  9996  dif1card  10005  numacn  10044  kmlem2  10146  dju1en  10166  ackbij1lem1  10215  ackbij1lem18  10232  fin23lem26  10320  isfin1-3  10381  axdc3lem4  10448  unsnen  10548  fpwwe2lem12  10637  ssxr  11283  fzpreddisj  13550  fzp1disj  13560  prinfzo0  13671  fzennn  13933  hashunsng  14352  hashunsngx  14353  hashxplem  14393  hashmap  14395  hashbclem  14411  hashf1lem1  14415  hashf1lem1OLD  14416  fsumsplitsn  15690  sumtp  15695  fsumsplitsnun  15701  fsum2dlem  15716  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  isumltss  15794  fprodm1  15911  fprod2dlem  15924  fprodsplitsn  15933  fprodfvdvdsd  16277  bitsinv1  16383  bitsinvp1  16390  vdwmc2  16912  prmdvdsprmo  16975  structcnvcnv  17086  f1omvdco3  19317  psgnunilem5  19362  gsumzunsnd  19824  gsumunsnfd  19825  gsum2dlem2  19839  dprd2da  19912  ablfac1eulem  19942  ablfac1eu  19943  lbsextlem4  20774  fidomndrng  20926  cnfldfun  20956  mplmonmul  21591  psrbag0  21623  ist1-2  22851  locfindis  23034  xkohaus  23157  ptcmpfi  23317  flimsncls  23490  tmdgsum  23599  tsmsgsum  23643  imasdsf1olem  23879  reconnlem1  24342  fsumcn  24386  ovolfiniun  25018  volfiniun  25064  ovolioo  25085  mbfconstlem  25144  i1fima2  25196  i1fd  25198  itg1val2  25201  itgfsum  25344  itgsplitioo  25355  dvmptfsum  25492  lhop1lem  25530  lhop  25533  vieta1lem2  25824  chtprm  26657  perfectlem2  26733  noextend  27169  noextenddif  27171  noextendlt  27172  noextendgt  27173  nosupbnd2lem1  27218  nbgrssvwo2  28650  p1evtxdeqlem  28800  eupthp1  29500  eupth2eucrct  29501  trlsegvdeg  29511  ex-dif  29707  ex-in  29709  ex-hash  29737  pliguhgr  29770  ofpreima2  31922  padct  31975  fzdif2  32033  fzodif2  32034  cycpmco2f1  32314  elrspunsn  32578  lindsunlem  32740  esumrnmpt2  33097  esum2dlem  33121  carsgclctunlem1  33347  eulerpartlemt  33401  eulerpartgbij  33402  ballotlemfp1  33521  actfunsnf1o  33647  actfunsnrndisj  33648  chtvalz  33672  bnj1421  34084  f1resfz0f1d  34134  subfacp1lem5  34206  cvmliftlem4  34310  cvmliftlem5  34311  mrsubvrs  34544  gg-cnfldfun  35228  bj-xpimasn  35884  bj-xpima1snALT  35886  finixpnum  36521  poimirlem3  36539  poimirlem4  36540  poimirlem13  36549  poimirlem14  36550  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem27  36563  dvrelog2  40977  dvrelog3  40978  mapfzcons2  41505  jm2.23  41783  kelac2lem  41854  kelac2  41855  pwslnm  41884  arearect  42012  iunrelexp0  42501  gneispace  42933  disjiun2  43793  mpct  43948  volioc  44736  volico  44747  sge0iunmptlemfi  45177  sge0splitsn  45205  ismeannd  45231  fsumsplitsndif  46089  perfectALTVlem2  46438