Theorem difid 4325

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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  {crab 3396   ∖ cdif 3895  ∅c0 4282

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-rab 3397  df-dif 3901  df-nul 4283

This theorem is referenced by:  dif0  4327  difun2  4430  diftpsn3  4753  symdifid  5037  difxp1  6117  difxp2  6118  2oconcl  8424  oev2  8444  fin1a2lem13  10310  ruclem13  16153  strle1  17071  s1chn  18528  chnccats1  18533  chnccat  18534  efgi1  19635  frgpuptinv  19685  gsumdifsnd  19875  dprdsn  19952  ablfac1eulem  19988  fctop  22920  cctop  22922  topcld  22951  indiscld  23007  mretopd  23008  restcld  23088  conndisj  23332  csdfil  23810  ufinffr  23845  prdsxmslem2  24445  bcth3  25259  voliunlem3  25481  sltlpss  27854  slelss  27855  uhgr0vb  29052  uhgr0  29053  nbgr1vtx  29338  uvtx01vtx  29377  cplgr1v  29410  frgr1v  30253  1vwmgr  30258  difres  32582  imadifxp  32583  mptiffisupp  32678  difico  32770  fzodif1  32779  indconst1  32847  symgcom2  33060  cycpmrn  33119  tocyccntz  33120  lindssn  33350  lbslsat  33650  0elsiga  34148  prsiga  34165  fiunelcarsg  34350  sibf0  34368  probun  34453  ballotlemfp1  34526  onint1  36514  poimirlem22  37702  poimirlem30  37710  zrdivrng  38013  safesnsupfilb  43535  ntrk0kbimka  44156  clsk3nimkb  44157  ntrclscls00  44183  ntrclskb  44186  ntrneicls11  44207  compne  44557  fzdifsuc2  45435  dvmptfprodlem  46066  fouriercn  46354  prsal  46440  caragenuncllem  46634  carageniuncllem1  46643  caratheodorylem1  46648  gsumdifsndf  48305