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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  {crab 3399   ∖ cdif 3898  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400  df-dif 3904  df-nul 4286

This theorem is referenced by:  dif0  4330  difun2  4433  diftpsn3  4758  symdifid  5042  difxp1  6123  difxp2  6124  2oconcl  8430  oev2  8450  fin1a2lem13  10322  ruclem13  16167  strle1  17085  s1chn  18543  chnccats1  18548  chnccat  18549  efgi1  19650  frgpuptinv  19700  gsumdifsnd  19890  dprdsn  19967  ablfac1eulem  20003  fctop  22948  cctop  22950  topcld  22979  indiscld  23035  mretopd  23036  restcld  23116  conndisj  23360  csdfil  23838  ufinffr  23873  prdsxmslem2  24473  bcth3  25287  voliunlem3  25509  ltslpss  27904  leslss  27905  uhgr0vb  29145  uhgr0  29146  nbgr1vtx  29431  uvtx01vtx  29470  cplgr1v  29503  frgr1v  30346  1vwmgr  30351  difres  32675  imadifxp  32676  mptiffisupp  32772  difico  32863  fzodif1  32872  indconst1  32940  symgcom2  33166  cycpmrn  33225  tocyccntz  33226  lindssn  33459  lbslsat  33773  0elsiga  34271  prsiga  34288  fiunelcarsg  34473  sibf0  34491  probun  34576  ballotlemfp1  34649  onint1  36643  poimirlem22  37839  poimirlem30  37847  zrdivrng  38150  safesnsupfilb  43655  ntrk0kbimka  44276  clsk3nimkb  44277  ntrclscls00  44303  ntrclskb  44306  ntrneicls11  44327  compne  44677  fzdifsuc2  45554  dvmptfprodlem  46184  fouriercn  46472  prsal  46558  caragenuncllem  46752  carageniuncllem1  46761  caratheodorylem1  46766  gsumdifsndf  48423