Theorem difid 4328

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147  {crab 3416   ∖ cdif 4048  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rab 3417  df-dif 4050  df-nul 4282

This theorem is used by:  dif0  4330  difun2  4440  diftpsn3  4765  symdifid  5050  difxp1  6169  difxp2  6170  2oconcl  8542  oev2  8562  fin1a2lem13  10520  indconst1  12363  ruclem13  16442  strle1  17368  s1chn  18826  chnccats1  18831  chnccat  18832  efgi1  19968  frgpuptinv  20018  gsumdifsnd  20208  dprdsn  20285  ablfac1eulem  20321  fctop  23355  cctop  23357  topcld  23386  indiscld  23442  mretopd  23443  restcld  23523  conndisj  23767  csdfil  24246  ufinffr  24281  prdsxmslem2  24881  bcth3  25685  voliunlem3  25906  ltslpss  28327  leslss  28328  uhgr0vb  29683  uhgr0  29684  nbgr1vtx  29972  uvtx01vtx  30011  cplgr1v  30044  frgr1v  30905  1vwmgr  30910  difres  33269  imadifxp  33270  mptiffisupp  33360  difico  33448  fzodif1  33457  symgcom2  33721  cycpmrn  33780  tocyccntz  33781  lindssn  34017  lbslsat  34331  0elsiga  34829  prsiga  34846  fiunelcarsg  35031  sibf0  35049  probun  35134  ballotlemfp1  35207  onint1  37428  poimirlem22  38765  poimirlem30  38773  zrdivrng  39090  safesnsupfilb  44622  ntrk0kbimka  45242  clsk3nimkb  45243  ntrclscls00  45269  ntrclskb  45272  ntrneicls11  45293  compne  45626  fzdifsuc2  46541  dvmptfprodlem  47169  fouriercn  47457  prsal  47543  caragenuncllem  47737  carageniuncllem1  47746  caratheodorylem1  47751  gsumdifsndf  49493