Theorem difid 4356

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  {crab 3420   ∖ cdif 3928  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-rab 3421  df-dif 3934  df-nul 4314

This theorem is referenced by:  dif0  4358  difun2  4461  diftpsn3  4783  symdifid  5068  difxp1  6159  difxp2  6160  2oconcl  8520  oev2  8540  fin1a2lem13  10431  ruclem13  16265  strle1  17182  efgi1  19707  frgpuptinv  19757  gsumdifsnd  19947  dprdsn  20024  ablfac1eulem  20060  fctop  22947  cctop  22949  topcld  22978  indiscld  23034  mretopd  23035  restcld  23115  conndisj  23359  csdfil  23837  ufinffr  23872  prdsxmslem2  24473  bcth3  25288  voliunlem3  25510  sltlpss  27876  slelss  27877  uhgr0vb  29056  uhgr0  29057  nbgr1vtx  29342  uvtx01vtx  29381  cplgr1v  29414  frgr1v  30257  1vwmgr  30262  difres  32586  imadifxp  32587  mptiffisupp  32675  difico  32765  fzodif1  32774  s1chn  32995  chnccats1  33000  symgcom2  33100  cycpmrn  33159  tocyccntz  33160  lindssn  33398  lbslsat  33661  0elsiga  34150  prsiga  34167  fiunelcarsg  34353  sibf0  34371  probun  34456  ballotlemfp1  34529  onint1  36472  poimirlem22  37671  poimirlem30  37679  zrdivrng  37982  safesnsupfilb  43409  ntrk0kbimka  44030  clsk3nimkb  44031  ntrclscls00  44057  ntrclskb  44060  ntrneicls11  44081  compne  44432  fzdifsuc2  45306  dvmptfprodlem  45940  fouriercn  46228  prsal  46314  caragenuncllem  46508  carageniuncllem1  46517  caratheodorylem1  46522  gsumdifsndf  48123