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  28619  p1evtxdeqlem  28769  eupthp1  29469  eupth2eucrct  29470  trlsegvdeg  29480  ex-dif  29676  ex-in  29678  ex-hash  29706  pliguhgr  29739  ofpreima2  31891  padct  31944  fzdif2  32002  fzodif2  32003  cycpmco2f1  32283  elrspunsn  32547  lindsunlem  32709  esumrnmpt2  33066  esum2dlem  33090  carsgclctunlem1  33316  eulerpartlemt  33370  eulerpartgbij  33371  ballotlemfp1  33490  actfunsnf1o  33616  actfunsnrndisj  33617  chtvalz  33641  bnj1421  34053  f1resfz0f1d  34103  subfacp1lem5  34175  cvmliftlem4  34279  cvmliftlem5  34280  mrsubvrs  34513  bj-xpimasn  35836  bj-xpima1snALT  35838  finixpnum  36473  poimirlem3  36491  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem27  36515  dvrelog2  40929  dvrelog3  40930  mapfzcons2  41457  jm2.23  41735  kelac2lem  41806  kelac2  41807  pwslnm  41836  arearect  41964  iunrelexp0  42453  gneispace  42885  disjiun2  43745  mpct  43900  volioc  44688  volico  44699  sge0iunmptlemfi  45129  sge0splitsn  45157  ismeannd  45183  fsumsplitsndif  46041  perfectALTVlem2  46390