Theorem difid 4330

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  {crab 3401   ∖ cdif 3900  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3402  df-dif 3906  df-nul 4288

This theorem is referenced by:  dif0  4332  difun2  4435  diftpsn3  4760  symdifid  5044  difxp1  6131  difxp2  6132  2oconcl  8440  oev2  8460  fin1a2lem13  10334  ruclem13  16179  strle1  17097  s1chn  18555  chnccats1  18560  chnccat  18561  efgi1  19662  frgpuptinv  19712  gsumdifsnd  19902  dprdsn  19979  ablfac1eulem  20015  fctop  22960  cctop  22962  topcld  22991  indiscld  23047  mretopd  23048  restcld  23128  conndisj  23372  csdfil  23850  ufinffr  23885  prdsxmslem2  24485  bcth3  25299  voliunlem3  25521  ltslpss  27916  leslss  27917  uhgr0vb  29157  uhgr0  29158  nbgr1vtx  29443  uvtx01vtx  29482  cplgr1v  29515  frgr1v  30358  1vwmgr  30363  difres  32686  imadifxp  32687  mptiffisupp  32782  difico  32873  fzodif1  32882  indconst1  32950  symgcom2  33177  cycpmrn  33236  tocyccntz  33237  lindssn  33470  lbslsat  33793  0elsiga  34291  prsiga  34308  fiunelcarsg  34493  sibf0  34511  probun  34596  ballotlemfp1  34669  onint1  36662  poimirlem22  37887  poimirlem30  37895  zrdivrng  38198  safesnsupfilb  43768  ntrk0kbimka  44389  clsk3nimkb  44390  ntrclscls00  44416  ntrclskb  44419  ntrneicls11  44440  compne  44790  fzdifsuc2  45666  dvmptfprodlem  46296  fouriercn  46584  prsal  46670  caragenuncllem  46864  carageniuncllem1  46873  caratheodorylem1  46878  gsumdifsndf  48535