![]() |
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 4218 | . . 3 ⊢ (𝐴 ∖ 𝐴) = ∅ | |
2 | 1 | difeq2i 3988 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅) |
3 | difdif 3999 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴 | |
4 | 2, 3 | eqtr3i 2804 | 1 ⊢ (𝐴 ∖ ∅) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∖ cdif 3828 ∅c0 4180 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rab 3097 df-v 3417 df-dif 3834 df-in 3838 df-ss 3845 df-nul 4181 |
This theorem is referenced by: unvdif 4307 disjdif2 4312 iinvdif 4869 symdif0 4874 dffv2 6586 2oconcl 7932 oe0m0 7949 oev2 7952 infdiffi 8917 cnfcom2lem 8960 m1bits 15652 mreexdomd 16781 efgi0 18607 vrgpinv 18658 frgpuptinv 18660 frgpnabllem1 18752 gsumval3 18784 gsumcllem 18785 dprddisj2 18914 0cld 21353 indiscld 21406 mretopd 21407 hauscmplem 21721 cfinfil 22208 csdfil 22209 filufint 22235 bcth3 23640 rembl 23847 volsup 23863 disjdifprg 30094 prsiga 31035 sigapildsyslem 31065 sigapildsys 31066 sxbrsigalem3 31175 0elcarsg 31210 carsgclctunlem3 31223 onint1 33317 csbdif 34048 lindsdom 34327 ntrclscls00 39779 ntrclskb 39782 compne 40191 prsal 42035 saluni 42041 caragen0 42220 carageniuncllem1 42235 aacllem 44270 |
Copyright terms: Public domain | W3C validator |