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 4180 | . 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅) | |
2 | in0 4347 | . 2 ⊢ (𝐴 ∩ ∅) = ∅ | |
3 | 1, 2 | eqtri 2846 | 1 ⊢ (∅ ∩ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∩ cin 3937 ∅c0 4293 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-rab 3149 df-v 3498 df-dif 3941 df-in 3945 df-nul 4294 |
This theorem is referenced by: pred0 6180 fresaunres2 6552 fnsuppeq0 7860 setsfun 16520 setsfun0 16521 indistopon 21611 fctop 21614 cctop 21616 restsn 21780 filconn 22493 chtdif 25737 ppidif 25742 ppi1 25743 cht1 25744 0res 30356 ofpreima2 30413 ordtconnlem1 31169 measvuni 31475 measinb 31482 cndprobnul 31697 ballotlemfp1 31751 ballotlemgun 31784 chtvalz 31902 mrsubvrs 32771 mblfinlem2 34932 ntrkbimka 40395 neicvgbex 40469 limsup0 41982 subsalsal 42649 nnfoctbdjlem 42744 |
Copyright terms: Public domain | W3C validator |