Theorem dif0 4332

Description: The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)

Assertion

Ref	Expression
dif0	⊢ (𝐴 ∖ ∅) = 𝐴

Proof of Theorem dif0

Step	Hyp	Ref	Expression
1		difid 4330	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4096	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4107	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2846	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1537   ∖ cdif 3933  ∅c0 4291

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  unvdif  4423  disjdif2  4428  iinvdif  5002  symdif0  5007  dffv2  6756  2oconcl  8128  oe0m0  8145  oev2  8148  infdiffi  9121  cnfcom2lem  9164  m1bits  15789  mreexdomd  16920  efgi0  18846  vrgpinv  18895  frgpuptinv  18897  frgpnabllem1  18993  gsumval3  19027  gsumcllem  19028  dprddisj2  19161  0cld  21646  indiscld  21699  mretopd  21700  hauscmplem  22014  cfinfil  22501  csdfil  22502  filufint  22528  bcth3  23934  rembl  24141  volsup  24157  disjdifprg  30325  tocycf  30759  tocyc01  30760  prsiga  31390  sigapildsyslem  31420  sigapildsys  31421  sxbrsigalem3  31530  0elcarsg  31565  carsgclctunlem3  31578  onint1  33797  csbdif  34609  lindsdom  34901  ntrclscls00  40436  ntrclskb  40439  compne  40793  prsal  42623  saluni  42629  caragen0  42808  carageniuncllem1  42823  aacllem  44922