Theorem difid 4382

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

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2106  {crab 3433   ∖ cdif 3960  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-rab 3434  df-dif 3966  df-nul 4340

This theorem is referenced by:  dif0  4384  difun2  4487  diftpsn3  4807  symdifid  5092  difxp1  6187  difxp2  6188  2oconcl  8540  oev2  8560  fin1a2lem13  10450  ruclem13  16275  strle1  17192  efgi1  19754  frgpuptinv  19804  gsumdifsnd  19994  dprdsn  20071  ablfac1eulem  20107  fctop  23027  cctop  23029  topcld  23059  indiscld  23115  mretopd  23116  restcld  23196  conndisj  23440  csdfil  23918  ufinffr  23953  prdsxmslem2  24558  bcth3  25379  voliunlem3  25601  sltlpss  27960  slelss  27961  uhgr0vb  29104  uhgr0  29105  nbgr1vtx  29390  uvtx01vtx  29429  cplgr1v  29462  frgr1v  30300  1vwmgr  30305  difres  32620  imadifxp  32621  mptiffisupp  32708  difico  32792  fzodif1  32801  symgcom2  33087  cycpmrn  33146  tocyccntz  33147  lindssn  33386  lbslsat  33644  0elsiga  34095  prsiga  34112  fiunelcarsg  34298  sibf0  34316  probun  34401  ballotlemfp1  34473  onint1  36432  poimirlem22  37629  poimirlem30  37637  zrdivrng  37940  safesnsupfilb  43408  ntrk0kbimka  44029  clsk3nimkb  44030  ntrclscls00  44056  ntrclskb  44059  ntrneicls11  44080  compne  44437  fzdifsuc2  45261  dvmptfprodlem  45900  fouriercn  46188  prsal  46274  caragenuncllem  46468  carageniuncllem1  46477  caratheodorylem1  46482  gsumdifsndf  48025