Theorem difid 4328

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

Syntax hints:  ¬ wn 3   = wceq 1559   ∈ wcel 2141  {crab 3413   ∖ cdif 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-rab 3414  df-dif 3907  df-nul 4286

This theorem is referenced by:  dif0  4330  difun2  4434  diftpsn3  4761  symdifid  5043  difxp1  6147  difxp2  6148  2oconcl  8467  oev2  8487  fin1a2lem13  10366  indconst1  12205  ruclem13  16257  strle1  17177  s1chn  18635  chnccats1  18640  chnccat  18641  efgi1  19744  frgpuptinv  19794  gsumdifsnd  19984  dprdsn  20061  ablfac1eulem  20097  fctop  23044  cctop  23046  topcld  23075  indiscld  23131  mretopd  23132  restcld  23212  conndisj  23456  csdfil  23934  ufinffr  23969  prdsxmslem2  24569  bcth3  25373  voliunlem3  25594  ltslpss  27978  leslss  27979  uhgr0vb  29219  uhgr0  29220  nbgr1vtx  29505  uvtx01vtx  29544  cplgr1v  29577  frgr1v  30419  1vwmgr  30424  difres  32749  imadifxp  32750  mptiffisupp  32845  difico  32935  fzodif1  32944  symgcom2  33225  cycpmrn  33284  tocyccntz  33285  lindssn  33525  lbslsat  33874  0elsiga  34372  prsiga  34389  fiunelcarsg  34574  sibf0  34592  probun  34677  ballotlemfp1  34750  onint1  36773  poimirlem22  38105  poimirlem30  38113  zrdivrng  38416  safesnsupfilb  43958  ntrk0kbimka  44579  clsk3nimkb  44580  ntrclscls00  44606  ntrclskb  44609  ntrneicls11  44630  compne  44980  fzdifsuc2  45853  dvmptfprodlem  46482  fouriercn  46770  prsal  46856  caragenuncllem  47050  carageniuncllem1  47059  caratheodorylem1  47064  gsumdifsndf  48767