Theorem disjsn 4711

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 4452	. 2 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}))
2		con2b 359	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥 ∈ 𝐴))
3		velsn 4642	. . . . 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 2817	. . 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 2108   ∩ cin 3950  ∅c0 4333  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334  df-sn 4627

This theorem is referenced by:  disjsn2  4712  ssdifsn  4788  ssunsn2  4827  opwo0id  5502  ndmima  6121  xpimasn  6205  snres0  6318  orddisj  6422  fnunop  6684  ressnop0  7173  ftpg  7176  funressn  7179  fsnunf  7205  fsnunfv  7207  frxp2  8169  frxp3  8176  frrlem11  8321  frrlem12  8322  wfrlem13OLD  8361  enpr2dOLD  9090  domdifsn  9094  domunsncan  9112  map2xp  9187  limensuci  9193  infensuc  9195  dif1enlem  9196  dif1enlemOLD  9197  unfi  9211  ssfi  9213  php  9247  phpOLD  9259  isinf  9296  isinfOLD  9297  ac6sfi  9320  fodomfi  9350  fodomfiOLD  9370  funsnfsupp  9432  disjcsn  9644  infdifsn  9697  cantnfp1lem3  9720  pm54.43  10041  dif1card  10050  numacn  10089  kmlem2  10192  dju1en  10212  ackbij1lem1  10259  ackbij1lem18  10276  fin23lem26  10365  isfin1-3  10426  axdc3lem4  10493  unsnen  10593  fpwwe2lem12  10682  ssxr  11330  fzpreddisj  13613  fzp1disj  13623  prinfzo0  13738  fzennn  14009  hashunsng  14431  hashunsngx  14432  hashxplem  14472  hashmap  14474  hashbclem  14491  hashf1lem1  14494  fsumsplitsn  15780  sumtp  15785  fsumsplitsnun  15791  fsum2dlem  15806  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  isumltss  15884  fprodm1  16003  fprod2dlem  16016  fprodsplitsn  16025  fprodfvdvdsd  16371  bitsinv1  16479  bitsinvp1  16486  vdwmc2  17017  prmdvdsprmo  17080  structcnvcnv  17190  f1omvdco3  19467  psgnunilem5  19512  gsumzunsnd  19974  gsumunsnfd  19975  gsum2dlem2  19989  dprd2da  20062  ablfac1eulem  20092  ablfac1eu  20093  fidomndrng  20774  lbsextlem4  21163  cnfldfun  21378  cnfldfunOLD  21391  mplmonmul  22054  psrbag0  22086  ist1-2  23355  locfindis  23538  xkohaus  23661  ptcmpfi  23821  flimsncls  23994  tmdgsum  24103  tsmsgsum  24147  imasdsf1olem  24383  reconnlem1  24848  fsumcn  24894  ovolfiniun  25536  volfiniun  25582  ovolioo  25603  mbfconstlem  25662  i1fima2  25714  i1fd  25716  itg1val2  25719  itgfsum  25862  itgsplitioo  25873  dvmptfsum  26013  lhop1lem  26052  lhop  26055  vieta1lem2  26353  chtprm  27196  perfectlem2  27274  noextend  27711  noextenddif  27713  noextendlt  27714  noextendgt  27715  nosupbnd2lem1  27760  nbgrssvwo2  29379  p1evtxdeqlem  29530  eupthp1  30235  eupth2eucrct  30236  trlsegvdeg  30246  ex-dif  30442  ex-in  30444  ex-hash  30472  pliguhgr  30505  ofpreima2  32676  padct  32731  fzdif2  32792  fzodif2  32793  cycpmco2f1  33144  elrgspnlem4  33249  elrspunsn  33457  lindsunlem  33675  esumrnmpt2  34069  esum2dlem  34093  carsgclctunlem1  34319  eulerpartlemt  34373  eulerpartgbij  34374  ballotlemfp1  34494  actfunsnf1o  34619  actfunsnrndisj  34620  chtvalz  34644  bnj1421  35056  f1resfz0f1d  35119  subfacp1lem5  35189  cvmliftlem4  35293  cvmliftlem5  35294  mrsubvrs  35527  bj-xpimasn  36956  bj-xpima1snALT  36958  finixpnum  37612  poimirlem3  37630  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem27  37654  dvrelog2  42065  dvrelog3  42066  mapfzcons2  42730  jm2.23  43008  kelac2lem  43076  kelac2  43077  pwslnm  43106  arearect  43227  iunrelexp0  43715  gneispace  44147  disjiun2  45063  mpct  45206  volioc  45987  volico  45998  sge0iunmptlemfi  46428  sge0splitsn  46456  ismeannd  46482  fsumsplitsndif  47360  perfectALTVlem2  47709  resinsn  48772  resinsnALT  48773  tposrescnv  48779  tposres3  48781