Theorem difid 4269

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

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  {crab 3074   ∖ cdif 3855  ∅c0 4225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-rab 3079  df-dif 3861  df-nul 4226

This theorem is referenced by:  dif0  4271  difun2  4377  diftpsn3  4692  symdifid  4974  difxp1  5994  difxp2  5995  2oconcl  8138  oev2  8158  fin1a2lem13  9872  ruclem13  15643  strle1  16650  efgi1  18914  frgpuptinv  18964  gsumdifsnd  19149  dprdsn  19226  ablfac1eulem  19262  fctop  21704  cctop  21706  topcld  21735  indiscld  21791  mretopd  21792  restcld  21872  conndisj  22116  csdfil  22594  ufinffr  22629  prdsxmslem2  23231  bcth3  24031  voliunlem3  24252  uhgr0vb  26964  uhgr0  26965  nbgr1vtx  27247  uvtx01vtx  27286  cplgr1v  27319  frgr1v  28155  1vwmgr  28160  difres  30461  imadifxp  30462  difico  30628  fzodif1  30638  symgcom2  30879  cycpmrn  30936  tocyccntz  30937  lindssn  31094  lbslsat  31220  0elsiga  31601  prsiga  31618  fiunelcarsg  31802  sibf0  31820  probun  31905  ballotlemfp1  31977  onint1  34187  poimirlem22  35359  poimirlem30  35367  zrdivrng  35671  ntrk0kbimka  41115  clsk3nimkb  41116  ntrclscls00  41142  ntrclskb  41145  ntrneicls11  41166  compne  41518  fzdifsuc2  42310  dvmptfprodlem  42952  fouriercn  43240  prsal  43326  caragenuncllem  43517  carageniuncllem1  43526  caratheodorylem1  43531  gsumdifsndf  44808