|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > difid | Structured version Visualization version GIF version | ||
| 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.) | 
| Ref | Expression | 
|---|---|
| difid | ⊢ (𝐴 ∖ 𝐴) = ∅ | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | dfdif2 3959 | . 2 ⊢ (𝐴 ∖ 𝐴) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | |
| 2 | dfnul3 4336 | . 2 ⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | |
| 3 | 1, 2 | eqtr4i 2767 | 1 ⊢ (𝐴 ∖ 𝐴) = ∅ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 = wceq 1539 ∈ wcel 2107 {crab 3435 ∖ cdif 3947 ∅c0 4332 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-rab 3436 df-dif 3953 df-nul 4333 | 
| This theorem is referenced by: dif0 4377 difun2 4480 diftpsn3 4801 symdifid 5086 difxp1 6184 difxp2 6185 2oconcl 8542 oev2 8562 fin1a2lem13 10453 ruclem13 16279 strle1 17196 efgi1 19740 frgpuptinv 19790 gsumdifsnd 19980 dprdsn 20057 ablfac1eulem 20093 fctop 23012 cctop 23014 topcld 23044 indiscld 23100 mretopd 23101 restcld 23181 conndisj 23425 csdfil 23903 ufinffr 23938 prdsxmslem2 24543 bcth3 25366 voliunlem3 25588 sltlpss 27946 slelss 27947 uhgr0vb 29090 uhgr0 29091 nbgr1vtx 29376 uvtx01vtx 29415 cplgr1v 29448 frgr1v 30291 1vwmgr 30296 difres 32614 imadifxp 32615 mptiffisupp 32703 difico 32786 fzodif1 32795 s1chn 33001 chnccats1 33006 symgcom2 33105 cycpmrn 33164 tocyccntz 33165 lindssn 33407 lbslsat 33668 0elsiga 34116 prsiga 34133 fiunelcarsg 34319 sibf0 34337 probun 34422 ballotlemfp1 34495 onint1 36451 poimirlem22 37650 poimirlem30 37658 zrdivrng 37961 safesnsupfilb 43436 ntrk0kbimka 44057 clsk3nimkb 44058 ntrclscls00 44084 ntrclskb 44087 ntrneicls11 44108 compne 44465 fzdifsuc2 45327 dvmptfprodlem 45964 fouriercn 46252 prsal 46338 caragenuncllem 46532 carageniuncllem1 46541 caratheodorylem1 46546 gsumdifsndf 48102 | 
| Copyright terms: Public domain | W3C validator |