Theorem disjdif 4434

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 3960	. 2 ⊢ 𝐴 ⊆ 𝐴
2		disjdifg 4433	. 2 ⊢ (𝐴 ⊆ 𝐴 → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Syntax hints:   = wceq 1570   ∖ cdif 3903   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4288

This theorem is referenced by:  disjdifr  4435  unvdif  4437  difdifdir  4453  fresaun  6751  fresaunres2  6752  fvsnun2  7183  undifixp  8933  undom  9054  enfixsn  9075  sbthlem7  9082  sbthlem8  9083  fodomr  9117  domss2  9125  mapdom2  9137  sucdom2  9188  dif1ennnALT  9238  fodomfir  9288  marypha1lem  9394  brwdom2  9536  infdifsn  9627  ackbij1lem12  10214  ssfin4  10295  hashinf  14373  hashfxnn0  14375  hashun2  14421  hashun3  14422  hashssdif  14451  hashfun  14476  hashf1lem2  14495  fsumless  15850  cvgcmpce  15872  incexclem  15892  incexc  15893  fprodsplit1f  16046  mreexexlem3d  17703  sylow2a  19690  gsumval3a  19974  dprd2da  20115  dpjcntz  20125  dpjdisj  20126  dpjlsm  20127  dpjidcl  20131  ablfac1eu  20146  pwssplit1  21161  frlmsslss2  21906  frlmssuvc1  21925  psdmul  22310  mdetdiaglem  22736  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  smadiadet  22808  nrmsep  23495  dfconn2  23557  fbncp  23977  filufint  24058  supnfcls  24158  flimfnfcls  24166  xrge0gsumle  24972  iundisj2  25689  volsup  25696  itg2cnlem2  25902  amgm  27133  wilthlem2  27211  rpvmasum2  27654  noextendseq  27809  noetasuplem2  27876  noetasuplem4  27878  noetainflem2  27880  noetainflem4  27882  axlowdimlem7  29276  axlowdimlem8  29277  axlowdimlem9  29278  axlowdimlem10  29279  axlowdimlem11  29280  axlowdimlem12  29281  unidifsnne  32860  iundisj2f  32913  fressupp  33011  padct  33041  resf1o  33053  iundisj2fi  33120  fprodeq02  33146  gsummptres2  33351  cycpmconjslem2  33453  cyc3conja  33455  gsumind  33643  elrspunidl  33714  lbsdiflsp0  33994  dimkerim  33995  locfinref  34209  esummono  34422  esumpad  34423  gsumesum  34427  ldgenpisyslem1  34531  measvuni  34582  pmeasmono  34692  eulerpartlemt  34739  tgoldbachgtde  35025  satfv1lem  35832  fullfunfnv  36416  fullfunfv  36417  opnbnd  36814  pibt2  38041  poimirlem6  38255  poimirlem7  38256  poimirlem15  38264  poimirlem22  38271  ismblfin  38290  evlselv  43301  fsuppssind  43305  diophrw  43470  diophren  43520  tfsconcatfn  44045  tfsconcatfv1  44046  tfsconcatfv2  44047  sumnnodd  46326  sge0ss  47106  meassle  47157  meaunle  47158  meadif  47173  meaiininclem  47180  disjdifb  49565  seposep  49681  iscnrm3rlem1  49695