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

Theorem disjsn 3693
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  |-  ( ( A  i^i  { B } )  =  (/)  <->  -.  B  e.  A )

Proof of Theorem disjsn
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 disj1 3497 . 2  |-  ( ( A  i^i  { B } )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  { B } ) )
2 con2b 324 . . . 4  |-  ( ( x  e.  A  ->  -.  x  e.  { B } )  <->  ( x  e.  { B }  ->  -.  x  e.  A ) )
3 elsn 3655 . . . . 5  |-  ( x  e.  { B }  <->  x  =  B )
43imbi1i 315 . . . 4  |-  ( ( x  e.  { B }  ->  -.  x  e.  A )  <->  ( x  =  B  ->  -.  x  e.  A ) )
5 imnan 411 . . . 4  |-  ( ( x  =  B  ->  -.  x  e.  A
)  <->  -.  ( x  =  B  /\  x  e.  A ) )
62, 4, 53bitri 262 . . 3  |-  ( ( x  e.  A  ->  -.  x  e.  { B } )  <->  -.  (
x  =  B  /\  x  e.  A )
)
76albii 1553 . 2  |-  ( A. x ( x  e.  A  ->  -.  x  e.  { B } )  <->  A. x  -.  (
x  =  B  /\  x  e.  A )
)
8 alnex 1530 . . 3  |-  ( A. x  -.  ( x  =  B  /\  x  e.  A )  <->  -.  E. x
( x  =  B  /\  x  e.  A
) )
9 df-clel 2279 . . 3  |-  ( B  e.  A  <->  E. x
( x  =  B  /\  x  e.  A
) )
108, 9xchbinxr 302 . 2  |-  ( A. x  -.  ( x  =  B  /\  x  e.  A )  <->  -.  B  e.  A )
111, 7, 103bitri 262 1  |-  ( ( A  i^i  { B } )  =  (/)  <->  -.  B  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684    i^i cin 3151   (/)c0 3455   {csn 3640
This theorem is referenced by:  disjsn2  3694  ssunsn2  3773  orddisj  4430  ndmima  5050  fnunsn  5351  ressnop0  5703  funressn  5706  fsnunf  5718  fsnunfv  5720  domdifsn  6945  domunsncan  6962  map2xp  7031  limensuci  7037  infensuc  7039  php  7045  isinf  7076  ac6sfi  7101  fodomfi  7135  marypha1lem  7186  infdifsn  7357  cantnfp1lem3  7382  pm54.43  7633  dif1card  7638  numacn  7676  kmlem2  7777  cda1en  7801  infpss  7843  ackbij1lem1  7846  ackbij1lem18  7863  ominf4  7938  fin23lem26  7951  isfin1-3  8012  axdc3lem4  8079  unsnen  8175  fpwwe2lem13  8264  ssxr  8892  fzp1disj  10843  fzennn  11030  hashunsng  11367  hashxplem  11385  hashmap  11387  hashbclem  11390  hashf1lem1  11393  cats1un  11476  fsum2dlem  12233  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  isumltss  12307  bitsinv1  12633  bitsinvp1  12640  isprm2lem  12765  vdwmc2  13026  structcnvcnv  13159  strlemor1  13235  gsumzaddlem  15203  gsumunsn  15221  gsum2d  15223  dprd2da  15277  ablfac1eulem  15307  ablfac1eu  15308  lbsextlem4  15914  fidomndrng  16048  mplmonmul  16208  psrbag0  16235  ist1-2  17075  xkohaus  17347  ptcmpfi  17504  flimsncls  17681  tmdgsum  17778  tsmsgsum  17821  imasdsf1olem  17937  reconnlem1  18331  fsumcn  18374  ovolfiniun  18860  volfiniun  18904  ovolioo  18925  mbfconstlem  18984  i1fima2  19034  i1fd  19036  itg1val2  19039  itgfsum  19181  itgsplitioo  19192  dvmptfsum  19322  lhop1lem  19360  lhop  19363  vieta1lem2  19691  chtprm  20391  perfectlem2  20469  ex-dif  20810  ex-in  20812  ballotlemfp1  23050  subfacp1lem5  23715  cvmliftlem4  23819  cvmliftlem5  23820  eupap1  23900  eupath2lem3  23903  vdegp1ai  23908  vdegp1bi  23909  wfrlem13  24268  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  locfindis  26305  mapfzcons2  26796  ftp  26893  jm2.23  27089  kelac2lem  27162  kelac2  27163  pwslnm  27196  f1omvdco3  27392  psgnunilem5  27417  difprsng  28069  bnj1421  29072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-dif 3155  df-in 3159  df-nul 3456  df-sn 3646
  Copyright terms: Public domain W3C validator