![]() |
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.) |
Ref | Expression |
---|---|
difid | ⊢ (𝐴 ∖ 𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3657 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | ssdif0 3975 | . 2 ⊢ (𝐴 ⊆ 𝐴 ↔ (𝐴 ∖ 𝐴) = ∅) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ (𝐴 ∖ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∖ cdif 3604 ⊆ wss 3607 ∅c0 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-dif 3610 df-in 3614 df-ss 3621 df-nul 3949 |
This theorem is referenced by: dif0 3983 difun2 4081 diftpsn3 4364 diftpsn3OLD 4365 symdifid 4631 difxp1 5594 difxp2 5595 2oconcl 7628 oev2 7648 fin1a2lem13 9272 ruclem13 15015 strle1 16020 efgi1 18180 frgpuptinv 18230 gsumdifsnd 18406 dprdsn 18481 ablfac1eulem 18517 fctop 20856 cctop 20858 topcld 20887 indiscld 20943 mretopd 20944 restcld 21024 conndisj 21267 csdfil 21745 ufinffr 21780 prdsxmslem2 22381 bcth3 23174 voliunlem3 23366 uhgr0vb 26012 uhgr0 26013 nbgr1vtx 26299 uvtx01vtx 26346 uvtxa01vtx0OLD 26348 cplgr1v 26382 frgr1v 27251 1vwmgr 27256 difres 29539 imadifxp 29540 difico 29673 0elsiga 30305 prsiga 30322 fiunelcarsg 30506 sibf0 30524 probun 30609 ballotlemfp1 30681 onint1 32573 poimirlem22 33561 poimirlem30 33569 zrdivrng 33882 ntrk0kbimka 38654 clsk3nimkb 38655 ntrclscls00 38681 ntrclskb 38684 ntrneicls11 38705 compne 38960 compneOLD 38961 fzdifsuc2 39838 dvmptfprodlem 40477 fouriercn 40767 prsal 40856 caragenuncllem 41047 carageniuncllem1 41056 caratheodorylem1 41061 gsumdifsndf 42469 |
Copyright terms: Public domain | W3C validator |