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

Theorem disjsn 3706
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 3510 . 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 3668 . . . . 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 1556 . 2  |-  ( A. x ( x  e.  A  ->  -.  x  e.  { B } )  <->  A. x  -.  (
x  =  B  /\  x  e.  A )
)
8 alnex 1533 . . 3  |-  ( A. x  -.  ( x  =  B  /\  x  e.  A )  <->  -.  E. x
( x  =  B  /\  x  e.  A
) )
9 df-clel 2292 . . 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 1530   E.wex 1531    = wceq 1632    e. wcel 1696    i^i cin 3164   (/)c0 3468   {csn 3653
This theorem is referenced by:  disjsn2  3707  ssunsn2  3789  orddisj  4446  ndmima  5066  fnunsn  5367  ressnop0  5719  funressn  5722  fsnunf  5734  fsnunfv  5736  domdifsn  6961  domunsncan  6978  map2xp  7047  limensuci  7053  infensuc  7055  php  7061  isinf  7092  ac6sfi  7117  fodomfi  7151  marypha1lem  7202  infdifsn  7373  cantnfp1lem3  7398  pm54.43  7649  dif1card  7654  numacn  7692  kmlem2  7793  cda1en  7817  infpss  7859  ackbij1lem1  7862  ackbij1lem18  7879  ominf4  7954  fin23lem26  7967  isfin1-3  8028  axdc3lem4  8095  unsnen  8191  fpwwe2lem13  8280  ssxr  8908  fzp1disj  10859  fzennn  11046  hashunsng  11383  hashxplem  11401  hashmap  11403  hashbclem  11406  hashf1lem1  11409  cats1un  11492  fsum2dlem  12249  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  isumltss  12323  bitsinv1  12649  bitsinvp1  12656  isprm2lem  12781  vdwmc2  13042  structcnvcnv  13175  strlemor1  13251  gsumzaddlem  15219  gsumunsn  15237  gsum2d  15239  dprd2da  15293  ablfac1eulem  15323  ablfac1eu  15324  lbsextlem4  15930  fidomndrng  16064  mplmonmul  16224  psrbag0  16251  ist1-2  17091  xkohaus  17363  ptcmpfi  17520  flimsncls  17697  tmdgsum  17794  tsmsgsum  17837  imasdsf1olem  17953  reconnlem1  18347  fsumcn  18390  ovolfiniun  18876  volfiniun  18920  ovolioo  18941  mbfconstlem  19000  i1fima2  19050  i1fd  19052  itg1val2  19055  itgfsum  19197  itgsplitioo  19208  dvmptfsum  19338  lhop1lem  19376  lhop  19379  vieta1lem2  19707  chtprm  20407  perfectlem2  20485  ex-dif  20826  ex-in  20828  ballotlemfp1  23066  subfacp1lem5  23730  cvmliftlem4  23834  cvmliftlem5  23835  eupap1  23915  eupath2lem3  23918  vdegp1ai  23923  vdegp1bi  23924  wfrlem13  24339  bsstrs  26249  nbssntrs  26250  bosser  26270  pdiveql  26271  locfindis  26408  mapfzcons2  26899  ftp  26996  jm2.23  27192  kelac2lem  27265  kelac2  27266  pwslnm  27299  f1omvdco3  27495  psgnunilem5  27520  bnj1421  29388
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-dif 3168  df-in 3172  df-nul 3469  df-sn 3659
  Copyright terms: Public domain W3C validator