Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dif0 | Structured version Visualization version GIF version |
Description: The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
Ref | Expression |
---|---|
dif0 | ⊢ (𝐴 ∖ ∅) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difid 3902 | . . 3 ⊢ (𝐴 ∖ 𝐴) = ∅ | |
2 | 1 | difeq2i 3687 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅) |
3 | difdif 3698 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴 | |
4 | 2, 3 | eqtr3i 2634 | 1 ⊢ (𝐴 ∖ ∅) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∖ cdif 3537 ∅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-ral 2901 df-rab 2905 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: unvdif 3994 disjdif2 3999 iinvdif 4528 symdif0 4533 dffv2 6181 2oconcl 7470 oe0m0 7487 oev2 7490 infdiffi 8438 cnfcom2lem 8481 m1bits 15000 mreexdomd 16133 efgi0 17956 vrgpinv 18005 frgpuptinv 18007 frgpnabllem1 18099 gsumval3 18131 gsumcllem 18132 dprddisj2 18261 0cld 20652 indiscld 20705 mretopd 20706 hauscmplem 21019 cfinfil 21507 csdfil 21508 filufint 21534 bcth3 22936 rembl 23115 volsup 23131 disjdifprg 28770 prsiga 29521 sigapildsyslem 29551 sigapildsys 29552 sxbrsigalem3 29661 0elcarsg 29696 carsgclctunlem3 29709 onint1 31618 csbdif 32347 lindsdom 32573 ntrclscls00 37384 ntrclskb 37387 prsal 39214 saluni 39220 caragen0 39396 carageniuncllem1 39411 aacllem 42356 |
Copyright terms: Public domain | W3C validator |