Theorem difid 4328

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  {crab 3414   ∖ cdif 3899  ∅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-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-rab 3415  df-dif 3905  df-nul 4283

This theorem is used by:  dif0  4330  difun2  4440  diftpsn3  4768  symdifid  5051  difxp1  6161  difxp2  6162  2oconcl  8494  oev2  8514  fin1a2lem13  10418  indconst1  12259  ruclem13  16336  strle1  17256  s1chn  18714  chnccats1  18719  chnccat  18720  efgi1  19854  frgpuptinv  19904  gsumdifsnd  20094  dprdsn  20171  ablfac1eulem  20207  fctop  23235  cctop  23237  topcld  23266  indiscld  23322  mretopd  23323  restcld  23403  conndisj  23647  csdfil  24126  ufinffr  24161  prdsxmslem2  24761  bcth3  25565  voliunlem3  25786  ltslpss  28181  leslss  28182  uhgr0vb  29537  uhgr0  29538  nbgr1vtx  29826  uvtx01vtx  29865  cplgr1v  29898  frgr1v  30759  1vwmgr  30764  difres  33081  imadifxp  33082  mptiffisupp  33173  difico  33262  fzodif1  33271  symgcom2  33532  cycpmrn  33591  tocyccntz  33592  lindssn  33819  lbslsat  34134  0elsiga  34632  prsiga  34649  fiunelcarsg  34835  sibf0  34853  probun  34938  ballotlemfp1  35011  onint1  37076  poimirlem22  38399  poimirlem30  38407  zrdivrng  38711  safesnsupfilb  44266  ntrk0kbimka  44887  clsk3nimkb  44888  ntrclscls00  44914  ntrclskb  44917  ntrneicls11  44938  compne  45272  fzdifsuc2  46151  dvmptfprodlem  46780  fouriercn  47068  prsal  47154  caragenuncllem  47348  carageniuncllem1  47357  caratheodorylem1  47362  gsumdifsndf  49104