Theorem difid 4301

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

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2108  {crab 3067   ∖ cdif 3880  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072  df-dif 3886  df-nul 4254

This theorem is referenced by:  dif0  4303  difun2  4411  diftpsn3  4732  symdifid  5012  difxp1  6057  difxp2  6058  2oconcl  8295  oev2  8315  fin1a2lem13  10099  ruclem13  15879  strle1  16787  efgi1  19242  frgpuptinv  19292  gsumdifsnd  19477  dprdsn  19554  ablfac1eulem  19590  fctop  22062  cctop  22064  topcld  22094  indiscld  22150  mretopd  22151  restcld  22231  conndisj  22475  csdfil  22953  ufinffr  22988  prdsxmslem2  23591  bcth3  24400  voliunlem3  24621  uhgr0vb  27345  uhgr0  27346  nbgr1vtx  27628  uvtx01vtx  27667  cplgr1v  27700  frgr1v  28536  1vwmgr  28541  difres  30840  imadifxp  30841  difico  31006  fzodif1  31016  symgcom2  31255  cycpmrn  31312  tocyccntz  31313  lindssn  31475  lbslsat  31601  0elsiga  31982  prsiga  31999  fiunelcarsg  32183  sibf0  32201  probun  32286  ballotlemfp1  32358  sltlpss  34014  onint1  34565  poimirlem22  35726  poimirlem30  35734  zrdivrng  36038  ntrk0kbimka  41538  clsk3nimkb  41539  ntrclscls00  41565  ntrclskb  41568  ntrneicls11  41589  compne  41948  fzdifsuc2  42739  dvmptfprodlem  43375  fouriercn  43663  prsal  43749  caragenuncllem  43940  carageniuncllem1  43949  caratheodorylem1  43954  gsumdifsndf  45263