Theorem disjdif 4425

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-nul 4279

This theorem is used by:  disjdifr  4426  unvdif  4428  difdifdir  4446  fresaun  6753  fresaunres2  6754  fvsnun2  7188  undifixp  8965  undom  9087  enfixsn  9108  sbthlem7  9115  sbthlem8  9116  fodomr  9150  domss2  9158  mapdom2  9170  sucdom2  9221  dif1ennnALT  9271  fodomfir  9322  marypha1lem  9428  brwdom2  9570  infdifsn  9661  ackbij1lem12  10311  ssfin4  10391  hashinf  14482  hashfxnn0  14484  hashun2  14530  hashun3  14531  hashssdif  14560  hashfun  14585  hashf1lem2  14604  fsumless  15968  cvgcmpce  15990  incexclem  16010  incexc  16011  fprodsplit1f  16162  mreexexlem3d  17825  sylow2a  19838  gsumval3a  20122  dprd2da  20263  dpjcntz  20273  dpjdisj  20274  dpjlsm  20275  dpjidcl  20279  ablfac1eu  20294  pwssplit1  21339  frlmsslss2  22086  frlmssuvc1  22105  psdmul  22492  mdetdiaglem  22918  mdetrlin  22922  mdetrsca  22923  mdetralt  22928  smadiadet  22990  nrmsep  23680  dfconn2  23742  fbncp  24163  filufint  24244  supnfcls  24344  flimfnfcls  24352  xrge0gsumle  25158  iundisj2  25875  volsup  25882  itg2cnlem2  26088  amgm  27323  wilthlem2  27401  rpvmasum2  27844  noextendseq  28029  noetasuplem2  28096  noetasuplem4  28098  noetainflem2  28100  noetainflem4  28102  axlowdimlem7  29531  axlowdimlem8  29532  axlowdimlem9  29533  axlowdimlem10  29534  axlowdimlem11  29535  axlowdimlem12  29536  unidifsnne  33179  iundisj2f  33231  fressupp  33328  padct  33357  resf1o  33368  iundisj2fi  33435  fprodeq02  33461  gsummptres2  33660  cycpmconjslem2  33762  cyc3conja  33764  gsumind  33952  elrspunidl  34024  lbsdiflsp0  34304  dimkerim  34305  locfinref  34519  esummono  34732  esumpad  34733  gsumesum  34737  ldgenpisyslem1  34842  measvuni  34893  pmeasmono  35002  eulerpartlemt  35049  tgoldbachgtde  35335  satfv1lem  36213  fullfunfnv  36802  fullfunfv  36803  opnbnd  37205  pibt2  38433  poimirlem6  38637  poimirlem7  38638  poimirlem15  38646  poimirlem22  38653  ismblfin  38672  evlselv  43710  fsuppssind  43714  diophrw  43863  diophren  43913  tfsconcatfn  44433  tfsconcatfv1  44434  tfsconcatfv2  44435  sumnnodd  46735  sge0ss  47515  meassle  47566  meaunle  47567  meadif  47582  meaiininclem  47589  disjdifb  50013  seposep  50133  iscnrm3rlem1  50147