Theorem disjdif 4429

Description: A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
disjdif	⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		ssid 3935	. 2 ⊢ 𝐴 ⊆ 𝐴
2		disjdifg 4428	. 2 ⊢ (𝐴 ⊆ 𝐴 → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  disjdifr  4430  unvdif  4432  difdifdir  4450  fresaun  6775  fresaunres2  6776  fvsnun2  7211  undifixp  8990  undom  9112  enfixsn  9133  sbthlem7  9140  sbthlem8  9141  fodomr  9175  domss2  9183  mapdom2  9195  sucdom2  9246  dif1ennnALT  9296  fodomfir  9347  marypha1lem  9452  brwdom2  9594  infdifsn  9685  ackbij1lem12  10335  ssfin4  10415  hashinf  14506  hashfxnn0  14508  hashun2  14554  hashun3  14555  hashssdif  14584  hashfun  14609  hashf1lem2  14628  fsumless  15992  cvgcmpce  16014  incexclem  16034  incexc  16035  fprodsplit1f  16186  mreexexlem3d  17849  sylow2a  19863  gsumval3a  20147  dprd2da  20288  dpjcntz  20298  dpjdisj  20299  dpjlsm  20300  dpjidcl  20304  ablfac1eu  20319  pwssplit1  21364  frlmsslss2  22111  frlmssuvc1  22130  psdmul  22517  mdetdiaglem  22943  mdetrlin  22947  mdetrsca  22948  mdetralt  22953  smadiadet  23015  nrmsep  23705  dfconn2  23767  fbncp  24188  filufint  24269  supnfcls  24369  flimfnfcls  24377  xrge0gsumle  25183  iundisj2  25900  volsup  25907  itg2cnlem2  26113  amgm  27348  wilthlem2  27426  rpvmasum2  27869  noextendseq  28054  noetasuplem2  28121  noetasuplem4  28123  noetainflem2  28125  noetainflem4  28127  axlowdimlem7  29556  axlowdimlem8  29557  axlowdimlem9  29558  axlowdimlem10  29559  axlowdimlem11  29560  axlowdimlem12  29561  unidifsnne  33204  iundisj2f  33256  fressupp  33352  padct  33381  resf1o  33392  iundisj2fi  33459  fprodeq02  33485  gsummptres2  33684  cycpmconjslem2  33786  cyc3conja  33788  gsumind  33976  elrspunidl  34048  lbsdiflsp0  34328  dimkerim  34329  locfinref  34543  esummono  34756  esumpad  34757  gsumesum  34761  ldgenpisyslem1  34866  measvuni  34917  pmeasmono  35026  eulerpartlemt  35073  tgoldbachgtde  35359  satfv1lem  36294  fullfunfnv  36888  fullfunfv  36889  opnbnd  37291  pibt2  38532  poimirlem6  38736  poimirlem7  38737  poimirlem15  38745  poimirlem22  38752  ismblfin  38771  evlselv  43810  fsuppssind  43814  diophrw  43963  diophren  44013  tfsconcatfn  44532  tfsconcatfv1  44533  tfsconcatfv2  44534  sumnnodd  46847  sge0ss  47627  meassle  47678  meaunle  47679  meadif  47694  meaiininclem  47701  disjdifb  50125  seposep  50245  iscnrm3rlem1  50259