Theorem disjsn 3828

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.

Step	Hyp	Ref	Expression
1		disj1 3630	. 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 3789	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 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 ) )
6	2, 4, 5	3bitri 263	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1572	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1549	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2400	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 303	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 263	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   i^i cin 3279   (/)c0 3588   {csn 3774

This theorem is referenced by:  disjsn2  3829  ssunsn2  3918  orddisj  4579  ndmima  5200  funtpg  5460  fnunsn  5511  ressnop0  5872  ftpg  5875  funressn  5878  fsnunf  5890  fsnunfv  5892  domdifsn  7150  domunsncan  7167  map2xp  7236  limensuci  7242  infensuc  7244  php  7250  isinf  7281  ac6sfi  7310  fodomfi  7344  infdifsn  7567  cantnfp1lem3  7592  pm54.43  7843  dif1card  7848  numacn  7886  kmlem2  7987  cda1en  8011  ackbij1lem1  8056  ackbij1lem18  8073  fin23lem26  8161  isfin1-3  8222  axdc3lem4  8289  unsnen  8384  fpwwe2lem13  8473  ssxr  9101  fzp1disj  11061  fzennn  11262  hashunsng  11620  hashxplem  11651  hashmap  11653  hashbclem  11656  hashf1lem1  11659  cats1un  11745  fsum2dlem  12509  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  isumltss  12583  bitsinv1  12909  bitsinvp1  12916  isprm2lem  13041  vdwmc2  13302  structcnvcnv  13435  strlemor1  13511  gsumzaddlem  15481  gsumunsn  15499  gsum2d  15501  dprd2da  15555  ablfac1eulem  15585  ablfac1eu  15586  lbsextlem4  16188  fidomndrng  16322  mplmonmul  16482  psrbag0  16509  ist1-2  17365  xkohaus  17638  ptcmpfi  17798  flimsncls  17971  tmdgsum  18078  tsmsgsum  18121  restutopopn  18221  imasdsf1olem  18356  reconnlem1  18810  fsumcn  18853  ovolfiniun  19350  volfiniun  19394  ovolioo  19415  mbfconstlem  19474  i1fima2  19524  i1fd  19526  itg1val2  19529  itgfsum  19671  itgsplitioo  19682  dvmptfsum  19812  lhop1lem  19850  lhop  19853  vieta1lem2  20181  chtprm  20889  perfectlem2  20967  usgrares1  21377  2pthlem2  21549  eupap1  21651  eupath2lem3  21654  vdegp1ai  21659  vdegp1bi  21660  ex-dif  21684  ex-in  21686  sibfof  24607  ballotlemfp1  24702  subfacp1lem5  24823  cvmliftlem4  24928  cvmliftlem5  24929  fprodm1  25243  fprod2dlem  25257  wfrlem13  25482  locfindis  26275  mapfzcons2  26665  jm2.23  26957  kelac2lem  27030  kelac2  27031  pwslnm  27064  f1omvdco3  27260  psgnunilem5  27285  bnj1421  29117

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918  df-dif 3283  df-in 3287  df-nul 3589  df-sn 3780