Theorem difid 4317

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  {crab 3390   ∖ cdif 3887  ∅c0 4274

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 3391  df-dif 3893  df-nul 4275

This theorem is referenced by:  dif0  4319  difun2  4422  diftpsn3  4746  symdifid  5030  difxp1  6123  difxp2  6124  2oconcl  8431  oev2  8451  fin1a2lem13  10325  indconst1  12163  ruclem13  16200  strle1  17119  s1chn  18577  chnccats1  18582  chnccat  18583  efgi1  19687  frgpuptinv  19737  gsumdifsnd  19927  dprdsn  20004  ablfac1eulem  20040  fctop  22979  cctop  22981  topcld  23010  indiscld  23066  mretopd  23067  restcld  23147  conndisj  23391  csdfil  23869  ufinffr  23904  prdsxmslem2  24504  bcth3  25308  voliunlem3  25529  ltslpss  27914  leslss  27915  uhgr0vb  29155  uhgr0  29156  nbgr1vtx  29441  uvtx01vtx  29480  cplgr1v  29513  frgr1v  30356  1vwmgr  30361  difres  32685  imadifxp  32686  mptiffisupp  32781  difico  32871  fzodif1  32880  symgcom2  33160  cycpmrn  33219  tocyccntz  33220  lindssn  33453  lbslsat  33776  0elsiga  34274  prsiga  34291  fiunelcarsg  34476  sibf0  34494  probun  34579  ballotlemfp1  34652  onint1  36647  poimirlem22  37977  poimirlem30  37985  zrdivrng  38288  safesnsupfilb  43863  ntrk0kbimka  44484  clsk3nimkb  44485  ntrclscls00  44511  ntrclskb  44514  ntrneicls11  44535  compne  44885  fzdifsuc2  45761  dvmptfprodlem  46390  fouriercn  46678  prsal  46764  caragenuncllem  46958  carageniuncllem1  46967  caratheodorylem1  46972  gsumdifsndf  48669