![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0in | Structured version Visualization version GIF version |
Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
0in | ⊢ (∅ ∩ 𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incom 4199 | . 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅) | |
2 | in0 4393 | . 2 ⊢ (𝐴 ∩ ∅) = ∅ | |
3 | 1, 2 | eqtri 2753 | 1 ⊢ (∅ ∩ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∩ cin 3943 ∅c0 4322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-in 3951 df-nul 4323 |
This theorem is referenced by: pred0 6343 fresaunres2 6769 fnsuppeq0 8197 setsfun 17143 setsfun0 17144 indistopon 22948 fctop 22951 cctop 22953 restsn 23118 filconn 23831 chtdif 27135 ppidif 27140 ppi1 27141 cht1 27142 0res 32472 ofpreima2 32533 ordtconnlem1 33656 measvuni 33964 measinb 33971 cndprobnul 34188 ballotlemfp1 34242 ballotlemgun 34275 chtvalz 34392 mrsubvrs 35263 mblfinlem2 37262 ntrkbimka 43610 neicvgbex 43684 limsup0 45220 subsalsal 45885 nnfoctbdjlem 45981 |
Copyright terms: Public domain | W3C validator |