![]() |
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 4096 | . . 3 ⊢ (𝐴 ∖ 𝐴) = ∅ | |
2 | 1 | difeq2i 3876 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅) |
3 | difdif 3887 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴 | |
4 | 2, 3 | eqtr3i 2795 | 1 ⊢ (𝐴 ∖ ∅) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∖ cdif 3720 ∅c0 4063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rab 3070 df-v 3353 df-dif 3726 df-in 3730 df-ss 3737 df-nul 4064 |
This theorem is referenced by: unvdif 4185 disjdif2 4190 iinvdif 4727 symdif0 4732 dffv2 6415 2oconcl 7741 oe0m0 7758 oev2 7761 infdiffi 8723 cnfcom2lem 8766 m1bits 15370 mreexdomd 16517 efgi0 18340 vrgpinv 18389 frgpuptinv 18391 frgpnabllem1 18483 gsumval3 18515 gsumcllem 18516 dprddisj2 18646 0cld 21063 indiscld 21116 mretopd 21117 hauscmplem 21430 cfinfil 21917 csdfil 21918 filufint 21944 bcth3 23347 rembl 23528 volsup 23544 disjdifprg 29726 prsiga 30534 sigapildsyslem 30564 sigapildsys 30565 sxbrsigalem3 30674 0elcarsg 30709 carsgclctunlem3 30722 onint1 32785 csbdif 33508 lindsdom 33736 ntrclscls00 38890 ntrclskb 38893 compne 39169 prsal 41052 saluni 41058 caragen0 41237 carageniuncllem1 41252 aacllem 43075 |
Copyright terms: Public domain | W3C validator |