Theorem difid 4332

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

Syntax hints:  ¬ wn 3   = wceq 1563   ∈ wcel 2145  {crab 3417   ∖ cdif 3904  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-rab 3418  df-dif 3910  df-nul 4289

This theorem is referenced by:  dif0  4334  difun2  4438  diftpsn3  4765  symdifid  5049  difxp1  6154  difxp2  6155  2oconcl  8476  oev2  8496  fin1a2lem13  10384  indconst1  12222  ruclem13  16288  strle1  17208  s1chn  18666  chnccats1  18671  chnccat  18672  efgi1  19782  frgpuptinv  19832  gsumdifsnd  20022  dprdsn  20099  ablfac1eulem  20135  fctop  23122  cctop  23124  topcld  23153  indiscld  23209  mretopd  23210  restcld  23290  conndisj  23534  csdfil  24012  ufinffr  24047  prdsxmslem2  24647  bcth3  25451  voliunlem3  25672  ltslpss  28059  leslss  28060  uhgr0vb  29331  uhgr0  29332  nbgr1vtx  29617  uvtx01vtx  29656  cplgr1v  29689  frgr1v  30531  1vwmgr  30536  difres  32855  imadifxp  32856  mptiffisupp  32950  difico  33040  fzodif1  33049  symgcom2  33317  cycpmrn  33376  tocyccntz  33377  lindssn  33607  lbslsat  33923  0elsiga  34421  prsiga  34438  fiunelcarsg  34623  sibf0  34641  probun  34726  ballotlemfp1  34799  onint1  36822  poimirlem22  38153  poimirlem30  38161  zrdivrng  38464  safesnsupfilb  44006  ntrk0kbimka  44627  clsk3nimkb  44628  ntrclscls00  44654  ntrclskb  44657  ntrneicls11  44678  compne  45014  fzdifsuc2  45887  dvmptfprodlem  46516  fouriercn  46804  prsal  46890  caragenuncllem  47084  carageniuncllem1  47093  caratheodorylem1  47098  gsumdifsndf  48801