Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0dif | Structured version Visualization version GIF version |
Description: The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
Ref | Expression |
---|---|
0dif | ⊢ (∅ ∖ 𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss 4066 | . 2 ⊢ (∅ ∖ 𝐴) ⊆ ∅ | |
2 | ss0 4332 | . 2 ⊢ ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∅ ∖ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∖ cdif 3884 ⊆ wss 3887 ∅c0 4256 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-dif 3890 df-in 3894 df-ss 3904 df-nul 4257 |
This theorem is referenced by: symdif0 5014 fresaun 6645 dffv2 6863 ablfac1eulem 19675 itgioo 24980 nbgr0vtx 27723 imadifxp 30940 sibf0 32301 ballotlemfval0 32462 ballotlemgun 32491 satf0 33334 mdvval 33466 newval 34039 fzdifsuc2 42849 ibliooicc 43512 disjdifb 46155 |
Copyright terms: Public domain | W3C validator |