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 4166 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
2 | ne0i 4297 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | |
3 | 1, 2 | sylbir 236 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ≠ wne 3013 ∩ cin 3932 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-v 3494 df-dif 3936 df-in 3940 df-nul 4289 |
This theorem is referenced by: minel 4411 disji 5040 disjiun 5044 onnseq 7970 uniinqs 8366 en3lplem1 9063 cplem1 9306 fpwwe2lem12 10051 limsupgre 14826 lmcls 21838 conncn 21962 iunconnlem 21963 conncompclo 21971 2ndcsep 21995 lfinpfin 22060 locfincmp 22062 txcls 22140 pthaus 22174 qtopeu 22252 trfbas2 22379 filss 22389 zfbas 22432 fmfnfm 22494 tsmsfbas 22663 restmetu 23107 qdensere 23305 reperflem 23353 reconnlem1 23361 metds0 23385 metnrmlem1a 23393 minveclem3b 23958 ovolicc2lem5 24049 taylfval 24874 wlk1walk 27347 wwlksm1edg 27586 disjif 30256 disjif2 30259 subfacp1lem6 32329 erdszelem5 32339 pconnconn 32375 cvmseu 32420 neibastop2lem 33605 topdifinffinlem 34510 sstotbnd3 34935 brtrclfv2 39950 corcltrcl 39962 disjinfi 41330 |
Copyright terms: Public domain | W3C validator |