Theorem difid 4316

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  {crab 3389   ∖ cdif 3886  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390  df-dif 3892  df-nul 4274

This theorem is referenced by:  dif0  4318  difun2  4421  diftpsn3  4747  symdifid  5029  difxp1  6129  difxp2  6130  2oconcl  8438  oev2  8458  fin1a2lem13  10334  indconst1  12172  ruclem13  16209  strle1  17128  s1chn  18586  chnccats1  18591  chnccat  18592  efgi1  19696  frgpuptinv  19746  gsumdifsnd  19936  dprdsn  20013  ablfac1eulem  20049  fctop  22969  cctop  22971  topcld  23000  indiscld  23056  mretopd  23057  restcld  23137  conndisj  23381  csdfil  23859  ufinffr  23894  prdsxmslem2  24494  bcth3  25298  voliunlem3  25519  ltslpss  27900  leslss  27901  uhgr0vb  29141  uhgr0  29142  nbgr1vtx  29427  uvtx01vtx  29466  cplgr1v  29499  frgr1v  30341  1vwmgr  30346  difres  32670  imadifxp  32671  mptiffisupp  32766  difico  32856  fzodif1  32865  symgcom2  33145  cycpmrn  33204  tocyccntz  33205  lindssn  33438  lbslsat  33760  0elsiga  34258  prsiga  34275  fiunelcarsg  34460  sibf0  34478  probun  34563  ballotlemfp1  34636  onint1  36631  poimirlem22  37963  poimirlem30  37971  zrdivrng  38274  safesnsupfilb  43845  ntrk0kbimka  44466  clsk3nimkb  44467  ntrclscls00  44493  ntrclskb  44496  ntrneicls11  44517  compne  44867  fzdifsuc2  45743  dvmptfprodlem  46372  fouriercn  46660  prsal  46746  caragenuncllem  46940  carageniuncllem1  46949  caratheodorylem1  46954  gsumdifsndf  48657