Theorem difid 4329

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  {crab 3396   ∖ cdif 3902  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3397  df-dif 3908  df-nul 4287

This theorem is referenced by:  dif0  4331  difun2  4434  diftpsn3  4756  symdifid  5039  difxp1  6118  difxp2  6119  2oconcl  8428  oev2  8448  fin1a2lem13  10325  ruclem13  16169  strle1  17087  efgi1  19618  frgpuptinv  19668  gsumdifsnd  19858  dprdsn  19935  ablfac1eulem  19971  fctop  22907  cctop  22909  topcld  22938  indiscld  22994  mretopd  22995  restcld  23075  conndisj  23319  csdfil  23797  ufinffr  23832  prdsxmslem2  24433  bcth3  25247  voliunlem3  25469  sltlpss  27840  slelss  27841  uhgr0vb  29035  uhgr0  29036  nbgr1vtx  29321  uvtx01vtx  29360  cplgr1v  29393  frgr1v  30233  1vwmgr  30238  difres  32562  imadifxp  32563  mptiffisupp  32649  difico  32739  fzodif1  32748  s1chn  32965  chnccats1  32970  symgcom2  33039  cycpmrn  33098  tocyccntz  33099  lindssn  33325  lbslsat  33588  0elsiga  34080  prsiga  34097  fiunelcarsg  34283  sibf0  34301  probun  34386  ballotlemfp1  34459  onint1  36422  poimirlem22  37621  poimirlem30  37629  zrdivrng  37932  safesnsupfilb  43391  ntrk0kbimka  44012  clsk3nimkb  44013  ntrclscls00  44039  ntrclskb  44042  ntrneicls11  44063  compne  44414  fzdifsuc2  45292  dvmptfprodlem  45926  fouriercn  46214  prsal  46300  caragenuncllem  46494  carageniuncllem1  46503  caratheodorylem1  46508  gsumdifsndf  48166