Theorem difid 4324

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2144  {crab 3412   ∖ cdif 4045  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-rab 3413  df-dif 4047  df-nul 4279

This theorem is used by:  dif0  4326  difun2  4436  diftpsn3  4761  symdifid  5046  difxp1  6155  difxp2  6156  2oconcl  8514  oev2  8534  fin1a2lem13  10493  indconst1  12336  ruclem13  16415  strle1  17341  s1chn  18799  chnccats1  18804  chnccat  18805  efgi1  19940  frgpuptinv  19990  gsumdifsnd  20180  dprdsn  20257  ablfac1eulem  20293  fctop  23327  cctop  23329  topcld  23358  indiscld  23414  mretopd  23415  restcld  23495  conndisj  23739  csdfil  24218  ufinffr  24253  prdsxmslem2  24853  bcth3  25657  voliunlem3  25878  ltslpss  28299  leslss  28300  uhgr0vb  29655  uhgr0  29656  nbgr1vtx  29944  uvtx01vtx  29983  cplgr1v  30016  frgr1v  30877  1vwmgr  30882  difres  33241  imadifxp  33242  mptiffisupp  33333  difico  33421  fzodif1  33430  symgcom2  33691  cycpmrn  33750  tocyccntz  33751  lindssn  33979  lbslsat  34294  0elsiga  34792  prsiga  34809  fiunelcarsg  34994  sibf0  35012  probun  35097  ballotlemfp1  35170  onint1  37329  poimirlem22  38653  poimirlem30  38661  zrdivrng  38980  safesnsupfilb  44512  ntrk0kbimka  45132  clsk3nimkb  45133  ntrclscls00  45159  ntrclskb  45162  ntrneicls11  45183  compne  45517  fzdifsuc2  46419  dvmptfprodlem  47047  fouriercn  47335  prsal  47421  caragenuncllem  47615  carageniuncllem1  47624  caratheodorylem1  47629  gsumdifsndf  49371