Theorem difid 4311

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

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  {crab 3392   ∖ cdif 3887  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-rab 3393  df-dif 3893  df-nul 4269

This theorem is referenced by:  dif0  4313  difun2  4416  diftpsn3  4742  symdifid  5023  difxp1  6123  difxp2  6124  2oconcl  8435  oev2  8455  fin1a2lem13  10332  indconst1  12170  ruclem13  16207  strle1  17126  s1chn  18584  chnccats1  18589  chnccat  18590  efgi1  19694  frgpuptinv  19744  gsumdifsnd  19934  dprdsn  20011  ablfac1eulem  20047  fctop  22994  cctop  22996  topcld  23025  indiscld  23081  mretopd  23082  restcld  23162  conndisj  23406  csdfil  23884  ufinffr  23919  prdsxmslem2  24519  bcth3  25323  voliunlem3  25544  ltslpss  27925  leslss  27926  uhgr0vb  29166  uhgr0  29167  nbgr1vtx  29452  uvtx01vtx  29491  cplgr1v  29524  frgr1v  30366  1vwmgr  30371  difres  32696  imadifxp  32697  mptiffisupp  32792  difico  32882  fzodif1  32891  symgcom2  33172  cycpmrn  33231  tocyccntz  33232  lindssn  33468  lbslsat  33807  0elsiga  34305  prsiga  34322  fiunelcarsg  34507  sibf0  34525  probun  34610  ballotlemfp1  34683  onint1  36684  poimirlem22  38016  poimirlem30  38024  zrdivrng  38327  safesnsupfilb  43869  ntrk0kbimka  44490  clsk3nimkb  44491  ntrclscls00  44517  ntrclskb  44520  ntrneicls11  44541  compne  44891  fzdifsuc2  45765  dvmptfprodlem  46394  fouriercn  46682  prsal  46768  caragenuncllem  46962  carageniuncllem1  46971  caratheodorylem1  46976  gsumdifsndf  48679