MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjsn Structured version   Visualization version   GIF version

Theorem disjsn 4449
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.
StepHypRef Expression
1 disj1 4227 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 350 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 4397 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 340 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 388 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 288 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1904 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1861 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 df-clel 2813 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 326 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 288 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2157  cin 3779  c0 4127  {csn 4381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-v 3404  df-dif 3783  df-in 3787  df-nul 4128  df-sn 4382
This theorem is referenced by:  disjsn2  4450  ssdifsn  4520  ssunsn2  4559  opwo0id  5161  ndmima  5723  xpimasn  5801  orddisj  5985  fnunsn  6216  ressnop0  6651  ftpg  6654  funressn  6657  fsnunf  6683  fsnunfv  6685  wfrlem13  7670  domdifsn  8289  domunsncan  8306  map2xp  8376  limensuci  8382  infensuc  8384  php  8390  isinf  8419  ac6sfi  8450  fodomfi  8485  funsnfsupp  8545  infdifsn  8808  cantnfp1lem3  8831  pm54.43  9116  dif1card  9123  numacn  9162  kmlem2  9265  cda1en  9289  ackbij1lem1  9334  ackbij1lem18  9351  fin23lem26  9439  isfin1-3  9500  axdc3lem4  9567  unsnen  9667  fpwwe2lem13  9756  ssxr  10399  fzpreddisj  12620  fzp1disj  12629  prinfzo0  12738  fzennn  12998  hashunsng  13406  hashxplem  13444  hashmap  13446  hashbclem  13460  hashf1lem1  13463  cats1un  13706  fsumsplitsn  14704  sumtp  14708  fsumsplitsnun  14714  fsumsplitsnunOLD  14716  fsum2dlem  14731  fsumabs  14762  fsumrlim  14772  fsumo1  14773  fsumiun  14782  isumltss  14809  fprodm1  14925  fprod2dlem  14938  fprodsplitsn  14947  fprodfvdvdsd  15285  bitsinv1  15390  bitsinvp1  15397  vdwmc2  15907  prmdvdsprmo  15970  structcnvcnv  16089  strlemor1OLD  16187  f1omvdco3  18077  psgnunilem5  18122  gsumzunsnd  18563  gsumunsnfd  18564  gsum2dlem2  18578  dprd2da  18650  ablfac1eulem  18680  ablfac1eu  18681  lbsextlem4  19377  fidomndrng  19523  mplmonmul  19680  psrbag0  19709  cnfldfunALT  19974  ist1-2  21373  locfindis  21555  xkohaus  21678  ptcmpfi  21838  flimsncls  22011  tmdgsum  22120  tsmsgsum  22163  imasdsf1olem  22399  reconnlem1  22850  fsumcn  22894  ovolfiniun  23492  volfiniun  23538  ovolioo  23559  mbfconstlem  23618  i1fima2  23670  i1fd  23672  itg1val2  23675  itgfsum  23817  itgsplitioo  23828  dvmptfsum  23962  lhop1lem  24000  lhop  24003  vieta1lem2  24290  chtprm  25103  perfectlem2  25179  nbgrssvwo2  26484  nbgrssvwo2OLD  26487  p1evtxdeqlem  26646  eupthp1  27399  eupth2eucrct  27400  trlsegvdeg  27410  ex-dif  27621  ex-in  27623  ex-hash  27651  pliguhgr  27679  ofpreima2  29803  padct  29834  fzdif2  29888  fzodif2  29889  esumrnmpt2  30465  esum2dlem  30489  carsgclctunlem1  30714  eulerpartlemt  30768  eulerpartgbij  30769  ballotlemfp1  30888  actfunsnf1o  31017  actfunsnrndisj  31018  chtvalz  31042  bnj1421  31442  subfacp1lem5  31498  cvmliftlem4  31602  cvmliftlem5  31603  mrsubvrs  31751  noextend  32149  noextenddif  32151  noextendlt  32152  noextendgt  32153  nosupbnd2lem1  32191  bj-disjcsn  33253  bj-xpimasn  33258  bj-xpima1snALT  33260  finixpnum  33713  poimirlem3  33731  poimirlem4  33732  poimirlem13  33741  poimirlem14  33742  poimirlem15  33743  poimirlem16  33744  poimirlem17  33745  poimirlem18  33746  poimirlem19  33747  poimirlem20  33748  poimirlem21  33749  poimirlem22  33750  poimirlem27  33755  mapfzcons2  37789  jm2.23  38069  kelac2lem  38140  kelac2  38141  pwslnm  38170  arearect  38306  iunrelexp0  38499  gneispace  38937  disjiun2  39724  mpct  39885  volioc  40672  volico  40684  sge0iunmptlemfi  41114  sge0splitsn  41142  ismeannd  41168  fsumsplitsndif  41923  perfectALTVlem2  42211
  Copyright terms: Public domain W3C validator