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  6156  difxp2  6157  2oconcl  8511  oev2  8531  fin1a2lem13  10490  indconst1  12333  ruclem13  16410  strle1  17336  s1chn  18794  chnccats1  18799  chnccat  18800  efgi1  19935  frgpuptinv  19985  gsumdifsnd  20175  dprdsn  20252  ablfac1eulem  20288  fctop  23322  cctop  23324  topcld  23353  indiscld  23409  mretopd  23410  restcld  23490  conndisj  23734  csdfil  24213  ufinffr  24248  prdsxmslem2  24848  bcth3  25652  voliunlem3  25873  ltslpss  28294  leslss  28295  uhgr0vb  29650  uhgr0  29651  nbgr1vtx  29939  uvtx01vtx  29978  cplgr1v  30011  frgr1v  30872  1vwmgr  30877  difres  33194  imadifxp  33195  mptiffisupp  33286  difico  33375  fzodif1  33384  symgcom2  33645  cycpmrn  33704  tocyccntz  33705  lindssn  33933  lbslsat  34248  0elsiga  34746  prsiga  34763  fiunelcarsg  34948  sibf0  34966  probun  35051  ballotlemfp1  35124  onint1  37237  poimirlem22  38560  poimirlem30  38568  zrdivrng  38887  safesnsupfilb  44418  ntrk0kbimka  45038  clsk3nimkb  45039  ntrclscls00  45065  ntrclskb  45068  ntrneicls11  45089  compne  45423  fzdifsuc2  46325  dvmptfprodlem  46953  fouriercn  47241  prsal  47327  caragenuncllem  47521  carageniuncllem1  47530  caratheodorylem1  47535  gsumdifsndf  49277