Theorem difid 4339

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  {crab 3405   ∖ cdif 3911  ∅c0 4296

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 2701

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 2708  df-cleq 2721  df-rab 3406  df-dif 3917  df-nul 4297

This theorem is referenced by:  dif0  4341  difun2  4444  diftpsn3  4766  symdifid  5051  difxp1  6138  difxp2  6139  2oconcl  8467  oev2  8487  fin1a2lem13  10365  ruclem13  16210  strle1  17128  efgi1  19651  frgpuptinv  19701  gsumdifsnd  19891  dprdsn  19968  ablfac1eulem  20004  fctop  22891  cctop  22893  topcld  22922  indiscld  22978  mretopd  22979  restcld  23059  conndisj  23303  csdfil  23781  ufinffr  23816  prdsxmslem2  24417  bcth3  25231  voliunlem3  25453  sltlpss  27819  slelss  27820  uhgr0vb  28999  uhgr0  29000  nbgr1vtx  29285  uvtx01vtx  29324  cplgr1v  29357  frgr1v  30200  1vwmgr  30205  difres  32529  imadifxp  32530  mptiffisupp  32616  difico  32706  fzodif1  32715  s1chn  32936  chnccats1  32941  symgcom2  33041  cycpmrn  33100  tocyccntz  33101  lindssn  33349  lbslsat  33612  0elsiga  34104  prsiga  34121  fiunelcarsg  34307  sibf0  34325  probun  34410  ballotlemfp1  34483  onint1  36437  poimirlem22  37636  poimirlem30  37644  zrdivrng  37947  safesnsupfilb  43407  ntrk0kbimka  44028  clsk3nimkb  44029  ntrclscls00  44055  ntrclskb  44058  ntrneicls11  44079  compne  44430  fzdifsuc2  45308  dvmptfprodlem  45942  fouriercn  46230  prsal  46316  caragenuncllem  46510  carageniuncllem1  46519  caratheodorylem1  46524  gsumdifsndf  48169