Theorem difid 4326

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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2111  {crab 3395   ∖ cdif 3899  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396  df-dif 3905  df-nul 4284

This theorem is referenced by:  dif0  4328  difun2  4431  diftpsn3  4754  symdifid  5035  difxp1  6112  difxp2  6113  2oconcl  8418  oev2  8438  fin1a2lem13  10300  ruclem13  16148  strle1  17066  s1chn  18523  chnccats1  18528  chnccat  18529  efgi1  19631  frgpuptinv  19681  gsumdifsnd  19871  dprdsn  19948  ablfac1eulem  19984  fctop  22917  cctop  22919  topcld  22948  indiscld  23004  mretopd  23005  restcld  23085  conndisj  23329  csdfil  23807  ufinffr  23842  prdsxmslem2  24442  bcth3  25256  voliunlem3  25478  sltlpss  27851  slelss  27852  uhgr0vb  29048  uhgr0  29049  nbgr1vtx  29334  uvtx01vtx  29373  cplgr1v  29406  frgr1v  30246  1vwmgr  30251  difres  32575  imadifxp  32576  mptiffisupp  32669  difico  32761  fzodif1  32770  symgcom2  33048  cycpmrn  33107  tocyccntz  33108  lindssn  33338  lbslsat  33624  0elsiga  34122  prsiga  34139  fiunelcarsg  34324  sibf0  34342  probun  34427  ballotlemfp1  34500  onint1  36482  poimirlem22  37681  poimirlem30  37689  zrdivrng  37992  safesnsupfilb  43450  ntrk0kbimka  44071  clsk3nimkb  44072  ntrclscls00  44098  ntrclskb  44101  ntrneicls11  44122  compne  44472  fzdifsuc2  45350  dvmptfprodlem  45981  fouriercn  46269  prsal  46355  caragenuncllem  46549  carageniuncllem1  46558  caratheodorylem1  46563  gsumdifsndf  48211