![]() |
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 4028 | . 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅) | |
2 | in0 4194 | . 2 ⊢ (𝐴 ∩ ∅) = ∅ | |
3 | 1, 2 | eqtri 2802 | 1 ⊢ (∅ ∩ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∩ cin 3791 ∅c0 4141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-dif 3795 df-in 3799 df-nul 4142 |
This theorem is referenced by: pred0 5963 fresaunres2 6326 fnsuppeq0 7605 setsfun 16290 setsfun0 16291 indistopon 21213 fctop 21216 cctop 21218 restsn 21382 filconn 22095 chtdif 25336 ppidif 25341 ppi1 25342 cht1 25343 ofpreima2 30031 ordtconnlem1 30568 measvuni 30875 measinb 30882 cndprobnul 31098 ballotlemfp1 31152 ballotlemgun 31185 chtvalz 31309 mrsubvrs 32018 mblfinlem2 34073 ntrkbimka 39292 limsup0 40834 subsalsal 41501 nnfoctbdjlem 41596 |
Copyright terms: Public domain | W3C validator |