Theorem difid 4333

Description: The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) (Revised by David Abernethy, 17-Jun-2012.)

Assertion

Ref	Expression
difid	⊢ (𝐴 ∖ 𝐴) = ∅

Proof of Theorem difid

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfdif2 3915	. 2 ⊢ (𝐴 ∖ 𝐴) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
2		dfnul3 4291	. 2 ⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
3	1, 2	eqtr4i 2789	1 ⊢ (𝐴 ∖ 𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1570   ∈ wcel 2143  {crab 3416   ∖ cdif 3903  ∅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-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-rab 3417  df-dif 3909  df-nul 4288

This theorem is referenced by:  dif0  4335  difun2  4443  diftpsn3  4771  symdifid  5054  difxp1  6164  difxp2  6165  2oconcl  8489  oev2  8509  fin1a2lem13  10397  indconst1  12232  ruclem13  16299  strle1  17219  s1chn  18677  chnccats1  18682  chnccat  18683  efgi1  19792  frgpuptinv  19842  gsumdifsnd  20032  dprdsn  20109  ablfac1eulem  20145  fctop  23142  cctop  23144  topcld  23173  indiscld  23229  mretopd  23230  restcld  23310  conndisj  23554  csdfil  24032  ufinffr  24067  prdsxmslem2  24667  bcth3  25471  voliunlem3  25692  ltslpss  28079  leslss  28080  uhgr0vb  29400  uhgr0  29401  nbgr1vtx  29686  uvtx01vtx  29725  cplgr1v  29758  frgr1v  30600  1vwmgr  30605  difres  32923  imadifxp  32924  mptiffisupp  33016  difico  33106  fzodif1  33115  symgcom2  33382  cycpmrn  33441  tocyccntz  33442  lindssn  33669  lbslsat  33984  0elsiga  34482  prsiga  34499  fiunelcarsg  34684  sibf0  34702  probun  34787  ballotlemfp1  34860  onint1  36938  poimirlem22  38271  poimirlem30  38279  zrdivrng  38582  safesnsupfilb  44124  ntrk0kbimka  44745  clsk3nimkb  44746  ntrclscls00  44772  ntrclskb  44775  ntrneicls11  44796  compne  45130  fzdifsuc2  46009  dvmptfprodlem  46638  fouriercn  46926  prsal  47012  caragenuncllem  47206  carageniuncllem1  47215  caratheodorylem1  47220  gsumdifsndf  48923