Theorem dif0 3950

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 3948	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 3725	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 3736	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2646	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1483   ∖ cdif 3571  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  unvdif  4042  disjdif2  4047  iinvdif  4592  symdif0  4597  dffv2  6271  2oconcl  7583  oe0m0  7600  oev2  7603  infdiffi  8555  cnfcom2lem  8598  m1bits  15162  mreexdomd  16310  efgi0  18133  vrgpinv  18182  frgpuptinv  18184  frgpnabllem1  18276  gsumval3  18308  gsumcllem  18309  dprddisj2  18438  0cld  20842  indiscld  20895  mretopd  20896  hauscmplem  21209  cfinfil  21697  csdfil  21698  filufint  21724  bcth3  23128  rembl  23308  volsup  23324  disjdifprg  29388  prsiga  30194  sigapildsyslem  30224  sigapildsys  30225  sxbrsigalem3  30334  0elcarsg  30369  carsgclctunlem3  30382  onint1  32448  csbdif  33171  lindsdom  33403  ntrclscls00  38364  ntrclskb  38367  compne  38643  prsal  40538  saluni  40544  caragen0  40720  carageniuncllem1  40735  aacllem  42547