Theorem difid 4371

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2107  {crab 3433   ∖ cdif 3946  ∅c0 4323

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434  df-dif 3952  df-nul 4324

This theorem is referenced by:  dif0  4373  difun2  4481  diftpsn3  4806  symdifid  5091  difxp1  6165  difxp2  6166  2oconcl  8503  oev2  8523  fin1a2lem13  10407  ruclem13  16185  strle1  17091  efgi1  19589  frgpuptinv  19639  gsumdifsnd  19829  dprdsn  19906  ablfac1eulem  19942  fctop  22507  cctop  22509  topcld  22539  indiscld  22595  mretopd  22596  restcld  22676  conndisj  22920  csdfil  23398  ufinffr  23433  prdsxmslem2  24038  bcth3  24848  voliunlem3  25069  sltlpss  27401  uhgr0vb  28332  uhgr0  28333  nbgr1vtx  28615  uvtx01vtx  28654  cplgr1v  28687  frgr1v  29524  1vwmgr  29529  difres  31831  imadifxp  31832  mptiffisupp  31915  difico  31994  fzodif1  32004  symgcom2  32245  cycpmrn  32302  tocyccntz  32303  lindssn  32494  lbslsat  32701  0elsiga  33112  prsiga  33129  fiunelcarsg  33315  sibf0  33333  probun  33418  ballotlemfp1  33490  onint1  35334  poimirlem22  36510  poimirlem30  36518  zrdivrng  36821  safesnsupfilb  42169  ntrk0kbimka  42790  clsk3nimkb  42791  ntrclscls00  42817  ntrclskb  42820  ntrneicls11  42841  compne  43200  fzdifsuc2  44020  dvmptfprodlem  44660  fouriercn  44948  prsal  45034  caragenuncllem  45228  carageniuncllem1  45237  caratheodorylem1  45242  gsumdifsndf  46591