Theorem difid 4398

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

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2108  {crab 3443   ∖ cdif 3973  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444  df-dif 3979  df-nul 4353

This theorem is referenced by:  dif0  4400  difun2  4504  diftpsn3  4827  symdifid  5110  difxp1  6196  difxp2  6197  2oconcl  8559  oev2  8579  fin1a2lem13  10481  ruclem13  16290  strle1  17205  efgi1  19763  frgpuptinv  19813  gsumdifsnd  20003  dprdsn  20080  ablfac1eulem  20116  fctop  23032  cctop  23034  topcld  23064  indiscld  23120  mretopd  23121  restcld  23201  conndisj  23445  csdfil  23923  ufinffr  23958  prdsxmslem2  24563  bcth3  25384  voliunlem3  25606  sltlpss  27963  slelss  27964  uhgr0vb  29107  uhgr0  29108  nbgr1vtx  29393  uvtx01vtx  29432  cplgr1v  29465  frgr1v  30303  1vwmgr  30308  difres  32622  imadifxp  32623  mptiffisupp  32705  difico  32788  fzodif1  32798  symgcom2  33077  cycpmrn  33136  tocyccntz  33137  lindssn  33371  lbslsat  33629  0elsiga  34078  prsiga  34095  fiunelcarsg  34281  sibf0  34299  probun  34384  ballotlemfp1  34456  onint1  36415  poimirlem22  37602  poimirlem30  37610  zrdivrng  37913  safesnsupfilb  43380  ntrk0kbimka  44001  clsk3nimkb  44002  ntrclscls00  44028  ntrclskb  44031  ntrneicls11  44052  compne  44410  fzdifsuc2  45225  dvmptfprodlem  45865  fouriercn  46153  prsal  46239  caragenuncllem  46433  carageniuncllem1  46442  caratheodorylem1  46447  gsumdifsndf  47904