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 4327 | . . 3 ⊢ (𝐴 ∖ 𝐴) = ∅ | |
2 | 1 | difeq2i 4093 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅) |
3 | difdif 4104 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴 | |
4 | 2, 3 | eqtr3i 2843 | 1 ⊢ (𝐴 ∖ ∅) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∖ cdif 3930 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 |
This theorem is referenced by: unvdif 4419 disjdif2 4424 iinvdif 4993 symdif0 4998 dffv2 6749 2oconcl 8117 oe0m0 8134 oev2 8137 infdiffi 9109 cnfcom2lem 9152 m1bits 15777 mreexdomd 16908 efgi0 18775 vrgpinv 18824 frgpuptinv 18826 frgpnabllem1 18922 gsumval3 18956 gsumcllem 18957 dprddisj2 19090 0cld 21574 indiscld 21627 mretopd 21628 hauscmplem 21942 cfinfil 22429 csdfil 22430 filufint 22456 bcth3 23861 rembl 24068 volsup 24084 disjdifprg 30253 tocycf 30686 tocyc01 30687 prsiga 31289 sigapildsyslem 31319 sigapildsys 31320 sxbrsigalem3 31429 0elcarsg 31464 carsgclctunlem3 31477 onint1 33694 csbdif 34488 lindsdom 34767 ntrclscls00 40294 ntrclskb 40297 compne 40650 prsal 42480 saluni 42486 caragen0 42665 carageniuncllem1 42680 aacllem 44830 |
Copyright terms: Public domain | W3C validator |