Theorem difid 4304

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

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2106  {crab 3068   ∖ cdif 3884  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rab 3073  df-dif 3890  df-nul 4257

This theorem is referenced by:  dif0  4306  difun2  4414  diftpsn3  4735  symdifid  5016  difxp1  6068  difxp2  6069  2oconcl  8333  oev2  8353  fin1a2lem13  10168  ruclem13  15951  strle1  16859  efgi1  19327  frgpuptinv  19377  gsumdifsnd  19562  dprdsn  19639  ablfac1eulem  19675  fctop  22154  cctop  22156  topcld  22186  indiscld  22242  mretopd  22243  restcld  22323  conndisj  22567  csdfil  23045  ufinffr  23080  prdsxmslem2  23685  bcth3  24495  voliunlem3  24716  uhgr0vb  27442  uhgr0  27443  nbgr1vtx  27725  uvtx01vtx  27764  cplgr1v  27797  frgr1v  28635  1vwmgr  28640  difres  30939  imadifxp  30940  difico  31104  fzodif1  31114  symgcom2  31353  cycpmrn  31410  tocyccntz  31411  lindssn  31573  lbslsat  31699  0elsiga  32082  prsiga  32099  fiunelcarsg  32283  sibf0  32301  probun  32386  ballotlemfp1  32458  sltlpss  34087  onint1  34638  poimirlem22  35799  poimirlem30  35807  zrdivrng  36111  ntrk0kbimka  41649  clsk3nimkb  41650  ntrclscls00  41676  ntrclskb  41679  ntrneicls11  41700  compne  42059  fzdifsuc2  42849  dvmptfprodlem  43485  fouriercn  43773  prsal  43859  caragenuncllem  44050  carageniuncllem1  44059  caratheodorylem1  44064  gsumdifsndf  45375