![]() |
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 3587 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | ssdif0 3896 | . 2 ⊢ (𝐴 ⊆ 𝐴 ↔ (𝐴 ∖ 𝐴) = ∅) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ (𝐴 ∖ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∖ cdif 3537 ⊆ wss 3540 ∅c0 3874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: dif0 3904 difun2 4000 diftpsn3 4273 diftpsn3OLD 4274 symdifid 4535 difxp1 5478 difxp2 5479 2oconcl 7470 oev2 7490 fin1a2lem13 9117 ruclem13 14810 strle1 15800 efgi1 17957 frgpuptinv 18007 gsumdifsnd 18183 dprdsn 18258 ablfac1eulem 18294 fctop 20618 cctop 20620 topcld 20649 indiscld 20705 mretopd 20706 restcld 20786 conndisj 21029 csdfil 21508 ufinffr 21543 prdsxmslem2 22144 bcth3 22936 voliunlem3 23127 uhgr0vb 25738 uhgr0 25739 uhgra0v 25839 usgra0v 25900 cusgra1v 25990 frgra1v 26525 1vwmgra 26530 difres 28795 imadifxp 28796 difico 28935 0elsiga 29504 prsiga 29521 fiunelcarsg 29705 sibf0 29723 probun 29808 ballotlemfp1 29880 onint1 31618 poimirlem22 32601 poimirlem30 32609 zrdivrng 32922 ntrk0kbimka 37357 clsk3nimkb 37358 ntrclscls00 37384 ntrclskb 37387 ntrneicls11 37408 compne 37665 fzdifsuc2 38466 dvmptfprodlem 38834 fouriercn 39125 prsal 39214 caragenuncllem 39402 carageniuncllem1 39411 caratheodorylem1 39416 nbgr1vtx 40580 uvtxa01vtx0 40623 cplgr1v 40652 frgr1v 41441 1vwmgr 41446 gsumdifsndf 41937 |
Copyright terms: Public domain | W3C validator |