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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4283

This theorem is used by:  disjdifr  4430  unvdif  4432  difdifdir  4450  fresaun  6750  fresaunres2  6751  fvsnun2  7185  undifixp  8945  undom  9067  enfixsn  9088  sbthlem7  9095  sbthlem8  9096  fodomr  9130  domss2  9138  mapdom2  9150  sucdom2  9201  dif1ennnALT  9251  fodomfir  9301  marypha1lem  9407  brwdom2  9549  infdifsn  9640  ackbij1lem12  10236  ssfin4  10316  hashinf  14403  hashfxnn0  14405  hashun2  14451  hashun3  14452  hashssdif  14481  hashfun  14506  hashf1lem2  14525  fsumless  15887  cvgcmpce  15909  incexclem  15929  incexc  15930  fprodsplit1f  16083  mreexexlem3d  17740  sylow2a  19752  gsumval3a  20036  dprd2da  20177  dpjcntz  20187  dpjdisj  20188  dpjlsm  20189  dpjidcl  20193  ablfac1eu  20208  pwssplit1  21249  frlmsslss2  21994  frlmssuvc1  22013  psdmul  22400  mdetdiaglem  22826  mdetrlin  22830  mdetrsca  22831  mdetralt  22836  smadiadet  22898  nrmsep  23588  dfconn2  23650  fbncp  24071  filufint  24152  supnfcls  24252  flimfnfcls  24260  xrge0gsumle  25066  iundisj2  25783  volsup  25790  itg2cnlem2  25996  amgm  27235  wilthlem2  27313  rpvmasum2  27756  noextendseq  27911  noetasuplem2  27978  noetasuplem4  27980  noetainflem2  27982  noetainflem4  27984  axlowdimlem7  29413  axlowdimlem8  29414  axlowdimlem9  29415  axlowdimlem10  29416  axlowdimlem11  29417  axlowdimlem12  29418  unidifsnne  33019  iundisj2f  33071  fressupp  33168  padct  33197  resf1o  33209  iundisj2fi  33276  fprodeq02  33302  gsummptres2  33501  cycpmconjslem2  33603  cyc3conja  33605  gsumind  33793  elrspunidl  33864  lbsdiflsp0  34144  dimkerim  34145  locfinref  34359  esummono  34572  esumpad  34573  gsumesum  34577  ldgenpisyslem1  34682  measvuni  34733  pmeasmono  34843  eulerpartlemt  34890  tgoldbachgtde  35176  satfv1lem  35949  fullfunfnv  36533  fullfunfv  36534  opnbnd  36952  pibt2  38179  poimirlem6  38383  poimirlem7  38384  poimirlem15  38392  poimirlem22  38399  ismblfin  38418  evlselv  43443  fsuppssind  43447  diophrw  43612  diophren  43662  tfsconcatfn  44187  tfsconcatfv1  44188  tfsconcatfv2  44189  sumnnodd  46468  sge0ss  47248  meassle  47299  meaunle  47300  meadif  47315  meaiininclem  47322  disjdifb  49746  seposep  49860  iscnrm3rlem1  49874