Theorem dif0 4341

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 4339	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4086	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4097	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2794	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1567   ∖ cdif 3910  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-nul 4295

This theorem is referenced by:  unvdif  4441  disjdif2  4446  csbdif  4491  iinvdif  5050  symdif0  5055  dffv2  6977  2oconcl  8488  oe0m0  8505  oev2  8508  infdiffi  9627  cnfcom2lem  9670  brttrcl2  9683  ttrcltr  9685  rnttrcl  9691  indconst0  12230  m1bits  16498  mreexdomd  17705  efgi0  19790  vrgpinv  19839  frgpuptinv  19841  frgpnabllem1  19943  gsumval3  19977  gsumcllem  19978  dprddisj2  20111  0cld  23164  indiscld  23217  mretopd  23218  hauscmplem  23532  cfinfil  24019  csdfil  24020  filufint  24046  bcth3  25459  rembl  25668  volsup  25684  new0  28023  disjdifprg  32861  tocycf  33378  tocyc01  33379  prsiga  34466  sigapildsyslem  34496  sigapildsys  34497  sxbrsigalem3  34607  0elcarsg  34642  carsgclctunlem3  34655  onint1  36883  lindsdom  38187  oe0rif  43938  tfsconcat0i  43998  ntrclscls00  44718  ntrclskb  44721  compne  45076  prsal  46958  saluni  46965  caragen0  47146  carageniuncllem1  47161  iscnrm3rlem4  49640  aacllem  50509