Theorem difid 4325

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 3908	. 2 ⊢ (𝐴 ∖ 𝐴) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
2		dfnul3 4283	. 2 ⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
3	1, 2	eqtr4i 2787	1 ⊢ (𝐴 ∖ 𝐴) = ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  {crab 3413   ∖ cdif 3896  ∅c0 4279

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-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-rab 3414  df-dif 3902  df-nul 4280

This theorem is used by:  dif0  4327  difun2  4437  diftpsn3  4765  symdifid  5047  difxp1  6155  difxp2  6156  2oconcl  8495  oev2  8515  fin1a2lem13  10471  indconst1  12314  ruclem13  16390  strle1  17316  s1chn  18774  chnccats1  18779  chnccat  18780  efgi1  19915  frgpuptinv  19965  gsumdifsnd  20155  dprdsn  20232  ablfac1eulem  20268  fctop  23302  cctop  23304  topcld  23333  indiscld  23389  mretopd  23390  restcld  23470  conndisj  23714  csdfil  24193  ufinffr  24228  prdsxmslem2  24828  bcth3  25632  voliunlem3  25853  ltslpss  28276  leslss  28277  uhgr0vb  29632  uhgr0  29633  nbgr1vtx  29921  uvtx01vtx  29960  cplgr1v  29993  frgr1v  30854  1vwmgr  30859  difres  33176  imadifxp  33177  mptiffisupp  33268  difico  33357  fzodif1  33366  symgcom2  33627  cycpmrn  33686  tocyccntz  33687  lindssn  33915  lbslsat  34230  0elsiga  34728  prsiga  34745  fiunelcarsg  34931  sibf0  34949  probun  35034  ballotlemfp1  35107  onint1  37207  poimirlem22  38528  poimirlem30  38536  zrdivrng  38855  safesnsupfilb  44377  ntrk0kbimka  44998  clsk3nimkb  44999  ntrclscls00  45025  ntrclskb  45028  ntrneicls11  45049  compne  45383  fzdifsuc2  46269  dvmptfprodlem  46898  fouriercn  47186  prsal  47272  caragenuncllem  47466  carageniuncllem1  47475  caratheodorylem1  47480  gsumdifsndf  49222