Theorem difid 4335

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2146  {crab 3419   ∖ cdif 3905  ∅c0 4289

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 2156  ax-ext 2738

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 2745  df-cleq 2758  df-rab 3420  df-dif 3911  df-nul 4290

This theorem is used by:  dif0  4337  difun2  4447  diftpsn3  4775  symdifid  5058  difxp1  6167  difxp2  6168  2oconcl  8497  oev2  8517  fin1a2lem13  10414  indconst1  12249  ruclem13  16323  strle1  17243  s1chn  18701  chnccats1  18706  chnccat  18707  efgi1  19822  frgpuptinv  19872  gsumdifsnd  20062  dprdsn  20139  ablfac1eulem  20175  fctop  23198  cctop  23200  topcld  23229  indiscld  23285  mretopd  23286  restcld  23366  conndisj  23610  csdfil  24088  ufinffr  24123  prdsxmslem2  24723  bcth3  25527  voliunlem3  25748  ltslpss  28138  leslss  28139  uhgr0vb  29459  uhgr0  29460  nbgr1vtx  29745  uvtx01vtx  29784  cplgr1v  29817  frgr1v  30659  1vwmgr  30664  difres  32982  imadifxp  32983  mptiffisupp  33075  difico  33165  fzodif1  33174  symgcom2  33435  cycpmrn  33494  tocyccntz  33495  lindssn  33722  lbslsat  34037  0elsiga  34535  prsiga  34552  fiunelcarsg  34738  sibf0  34756  probun  34841  ballotlemfp1  34914  onint1  37001  poimirlem22  38334  poimirlem30  38342  zrdivrng  38645  safesnsupfilb  44185  ntrk0kbimka  44806  clsk3nimkb  44807  ntrclscls00  44833  ntrclskb  44836  ntrneicls11  44857  compne  45191  fzdifsuc2  46070  dvmptfprodlem  46699  fouriercn  46987  prsal  47073  caragenuncllem  47267  carageniuncllem1  47276  caratheodorylem1  47281  gsumdifsndf  48987