Theorem difid 4342

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  {crab 3408   ∖ cdif 3914  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rab 3409  df-dif 3920  df-nul 4300

This theorem is referenced by:  dif0  4344  difun2  4447  diftpsn3  4769  symdifid  5054  difxp1  6141  difxp2  6142  2oconcl  8470  oev2  8490  fin1a2lem13  10372  ruclem13  16217  strle1  17135  efgi1  19658  frgpuptinv  19708  gsumdifsnd  19898  dprdsn  19975  ablfac1eulem  20011  fctop  22898  cctop  22900  topcld  22929  indiscld  22985  mretopd  22986  restcld  23066  conndisj  23310  csdfil  23788  ufinffr  23823  prdsxmslem2  24424  bcth3  25238  voliunlem3  25460  sltlpss  27826  slelss  27827  uhgr0vb  29006  uhgr0  29007  nbgr1vtx  29292  uvtx01vtx  29331  cplgr1v  29364  frgr1v  30207  1vwmgr  30212  difres  32536  imadifxp  32537  mptiffisupp  32623  difico  32713  fzodif1  32722  s1chn  32943  chnccats1  32948  symgcom2  33048  cycpmrn  33107  tocyccntz  33108  lindssn  33356  lbslsat  33619  0elsiga  34111  prsiga  34128  fiunelcarsg  34314  sibf0  34332  probun  34417  ballotlemfp1  34490  onint1  36444  poimirlem22  37643  poimirlem30  37651  zrdivrng  37954  safesnsupfilb  43414  ntrk0kbimka  44035  clsk3nimkb  44036  ntrclscls00  44062  ntrclskb  44065  ntrneicls11  44086  compne  44437  fzdifsuc2  45315  dvmptfprodlem  45949  fouriercn  46237  prsal  46323  caragenuncllem  46517  carageniuncllem1  46526  caratheodorylem1  46531  gsumdifsndf  48173