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

Theorem disjsn 3860
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 3662 . 2  |-  ( ( A  i^i  { B } )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  { B } ) )
2 con2b 325 . . . 4  |-  ( ( x  e.  A  ->  -.  x  e.  { B } )  <->  ( x  e.  { B }  ->  -.  x  e.  A ) )
3 elsn 3821 . . . . 5  |-  ( x  e.  { B }  <->  x  =  B )
43imbi1i 316 . . . 4  |-  ( ( x  e.  { B }  ->  -.  x  e.  A )  <->  ( x  =  B  ->  -.  x  e.  A ) )
5 imnan 412 . . . 4  |-  ( ( x  =  B  ->  -.  x  e.  A
)  <->  -.  ( x  =  B  /\  x  e.  A ) )
62, 4, 53bitri 263 . . 3  |-  ( ( x  e.  A  ->  -.  x  e.  { B } )  <->  -.  (
x  =  B  /\  x  e.  A )
)
76albii 1575 . 2  |-  ( A. x ( x  e.  A  ->  -.  x  e.  { B } )  <->  A. x  -.  (
x  =  B  /\  x  e.  A )
)
8 alnex 1552 . . 3  |-  ( A. x  -.  ( x  =  B  /\  x  e.  A )  <->  -.  E. x
( x  =  B  /\  x  e.  A
) )
9 df-clel 2431 . . 3  |-  ( B  e.  A  <->  E. x
( x  =  B  /\  x  e.  A
) )
108, 9xchbinxr 303 . 2  |-  ( A. x  -.  ( x  =  B  /\  x  e.  A )  <->  -.  B  e.  A )
111, 7, 103bitri 263 1  |-  ( ( A  i^i  { B } )  =  (/)  <->  -.  B  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725    i^i cin 3311   (/)c0 3620   {csn 3806
This theorem is referenced by:  disjsn2  3861  ssunsn2  3950  orddisj  4611  ndmima  5233  funtpg  5493  fnunsn  5544  ressnop0  5905  ftpg  5908  funressn  5911  fsnunf  5923  fsnunfv  5925  domdifsn  7183  domunsncan  7200  map2xp  7269  limensuci  7275  infensuc  7277  php  7283  isinf  7314  ac6sfi  7343  fodomfi  7377  infdifsn  7603  cantnfp1lem3  7628  pm54.43  7879  dif1card  7884  numacn  7922  kmlem2  8023  cda1en  8047  ackbij1lem1  8092  ackbij1lem18  8109  fin23lem26  8197  isfin1-3  8258  axdc3lem4  8325  unsnen  8420  fpwwe2lem13  8509  ssxr  9137  fzp1disj  11097  fzennn  11299  hashunsng  11657  hashxplem  11688  hashmap  11690  hashbclem  11693  hashf1lem1  11696  cats1un  11782  fsum2dlem  12546  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  isumltss  12620  bitsinv1  12946  bitsinvp1  12953  isprm2lem  13078  vdwmc2  13339  structcnvcnv  13472  strlemor1  13548  gsumzaddlem  15518  gsumunsn  15536  gsum2d  15538  dprd2da  15592  ablfac1eulem  15622  ablfac1eu  15623  lbsextlem4  16225  fidomndrng  16359  mplmonmul  16519  psrbag0  16546  ist1-2  17403  xkohaus  17677  ptcmpfi  17837  flimsncls  18010  tmdgsum  18117  tsmsgsum  18160  restutopopn  18260  imasdsf1olem  18395  reconnlem1  18849  fsumcn  18892  ovolfiniun  19389  volfiniun  19433  ovolioo  19454  mbfconstlem  19513  i1fima2  19563  i1fd  19565  itg1val2  19568  itgfsum  19710  itgsplitioo  19721  dvmptfsum  19851  lhop1lem  19889  lhop  19892  vieta1lem2  20220  chtprm  20928  perfectlem2  21006  usgrares1  21416  2pthlem2  21588  eupap1  21690  eupath2lem3  21693  vdegp1ai  21698  vdegp1bi  21699  ex-dif  21723  ex-in  21725  sibfof  24646  ballotlemfp1  24741  subfacp1lem5  24862  cvmliftlem4  24967  cvmliftlem5  24968  fprodm1  25282  fprod2dlem  25296  wfrlem13  25542  locfindis  26376  mapfzcons2  26766  jm2.23  27058  kelac2lem  27130  kelac2  27131  pwslnm  27164  f1omvdco3  27360  psgnunilem5  27385  bnj1421  29348
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-dif 3315  df-in 3319  df-nul 3621  df-sn 3812
  Copyright terms: Public domain W3C validator