![]() |
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 3920 | . 2 ⊢ (𝐴 ∖ 𝐴) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | |
2 | dfnul3 4287 | . 2 ⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | |
3 | 1, 2 | eqtr4i 2764 | 1 ⊢ (𝐴 ∖ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1542 ∈ wcel 2107 {crab 3406 ∖ cdif 3908 ∅c0 4283 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-rab 3407 df-dif 3914 df-nul 4284 |
This theorem is referenced by: dif0 4333 difun2 4441 diftpsn3 4763 symdifid 5048 difxp1 6118 difxp2 6119 2oconcl 8450 oev2 8470 fin1a2lem13 10353 ruclem13 16129 strle1 17035 efgi1 19508 frgpuptinv 19558 gsumdifsnd 19743 dprdsn 19820 ablfac1eulem 19856 fctop 22370 cctop 22372 topcld 22402 indiscld 22458 mretopd 22459 restcld 22539 conndisj 22783 csdfil 23261 ufinffr 23296 prdsxmslem2 23901 bcth3 24711 voliunlem3 24932 sltlpss 27258 uhgr0vb 28065 uhgr0 28066 nbgr1vtx 28348 uvtx01vtx 28387 cplgr1v 28420 frgr1v 29257 1vwmgr 29262 difres 31564 imadifxp 31565 mptiffisupp 31654 difico 31733 fzodif1 31743 symgcom2 31984 cycpmrn 32041 tocyccntz 32042 lindssn 32213 lbslsat 32368 0elsiga 32770 prsiga 32787 fiunelcarsg 32973 sibf0 32991 probun 33076 ballotlemfp1 33148 onint1 34967 poimirlem22 36146 poimirlem30 36154 zrdivrng 36458 safesnsupfilb 41778 ntrk0kbimka 42399 clsk3nimkb 42400 ntrclscls00 42426 ntrclskb 42429 ntrneicls11 42450 compne 42809 fzdifsuc2 43631 dvmptfprodlem 44271 fouriercn 44559 prsal 44645 caragenuncllem 44839 carageniuncllem1 44848 caratheodorylem1 44853 gsumdifsndf 46201 |
Copyright terms: Public domain | W3C validator |