![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inelcm | Structured version Visualization version GIF version |
Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
Ref | Expression |
---|---|
inelcm | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 4023 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
2 | ne0i 4150 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | |
3 | 1, 2 | sylbir 227 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2166 ≠ wne 2999 ∩ cin 3797 ∅c0 4144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-v 3416 df-dif 3801 df-in 3805 df-nul 4145 |
This theorem is referenced by: minel 4257 disji 4858 disjiun 4861 onnseq 7707 uniinqs 8092 en3lplem1 8784 cplem1 9029 fpwwe2lem12 9778 limsupgre 14589 lmcls 21477 conncn 21600 iunconnlem 21601 conncompclo 21609 2ndcsep 21633 lfinpfin 21698 locfincmp 21700 txcls 21778 pthaus 21812 qtopeu 21890 trfbas2 22017 filss 22027 zfbas 22070 fmfnfm 22132 tsmsfbas 22301 restmetu 22745 qdensere 22943 reperflem 22991 reconnlem1 22999 metds0 23023 metnrmlem1a 23031 minveclem3b 23596 ovolicc2lem5 23687 taylfval 24512 wlk1walk 26936 wwlksm1edg 27180 wwlksm1edgOLD 27181 disjif 29938 disjif2 29941 subfacp1lem6 31713 erdszelem5 31723 pconnconn 31759 cvmseu 31804 neibastop2lem 32893 topdifinffinlem 33740 sstotbnd3 34117 brtrclfv2 38860 corcltrcl 38872 disjinfi 40188 |
Copyright terms: Public domain | W3C validator |