Theorem difid 4375

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

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2107  {crab 3435   ∖ cdif 3947  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-rab 3436  df-dif 3953  df-nul 4333

This theorem is referenced by:  dif0  4377  difun2  4480  diftpsn3  4801  symdifid  5086  difxp1  6184  difxp2  6185  2oconcl  8542  oev2  8562  fin1a2lem13  10453  ruclem13  16279  strle1  17196  efgi1  19740  frgpuptinv  19790  gsumdifsnd  19980  dprdsn  20057  ablfac1eulem  20093  fctop  23012  cctop  23014  topcld  23044  indiscld  23100  mretopd  23101  restcld  23181  conndisj  23425  csdfil  23903  ufinffr  23938  prdsxmslem2  24543  bcth3  25366  voliunlem3  25588  sltlpss  27946  slelss  27947  uhgr0vb  29090  uhgr0  29091  nbgr1vtx  29376  uvtx01vtx  29415  cplgr1v  29448  frgr1v  30291  1vwmgr  30296  difres  32614  imadifxp  32615  mptiffisupp  32703  difico  32786  fzodif1  32795  s1chn  33001  chnccats1  33006  symgcom2  33105  cycpmrn  33164  tocyccntz  33165  lindssn  33407  lbslsat  33668  0elsiga  34116  prsiga  34133  fiunelcarsg  34319  sibf0  34337  probun  34422  ballotlemfp1  34495  onint1  36451  poimirlem22  37650  poimirlem30  37658  zrdivrng  37961  safesnsupfilb  43436  ntrk0kbimka  44057  clsk3nimkb  44058  ntrclscls00  44084  ntrclskb  44087  ntrneicls11  44108  compne  44465  fzdifsuc2  45327  dvmptfprodlem  45964  fouriercn  46252  prsal  46338  caragenuncllem  46532  carageniuncllem1  46541  caratheodorylem1  46546  gsumdifsndf  48102