![]() |
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 4025 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
2 | ne0i 4152 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | |
3 | 1, 2 | sylbir 227 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2164 ≠ wne 2999 ∩ cin 3797 ∅c0 4146 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 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 4147 |
This theorem is referenced by: minel 4259 disji 4860 disjiun 4863 onnseq 7712 uniinqs 8097 en3lplem1 8791 cplem1 9036 fpwwe2lem12 9785 limsupgre 14596 lmcls 21484 conncn 21607 iunconnlem 21608 conncompclo 21616 2ndcsep 21640 lfinpfin 21705 locfincmp 21707 txcls 21785 pthaus 21819 qtopeu 21897 trfbas2 22024 filss 22034 zfbas 22077 fmfnfm 22139 tsmsfbas 22308 restmetu 22752 qdensere 22950 reperflem 22998 reconnlem1 23006 metds0 23030 metnrmlem1a 23038 minveclem3b 23603 ovolicc2lem5 23694 taylfval 24519 wlk1walk 26943 wwlksm1edg 27187 wwlksm1edgOLD 27188 disjif 29934 disjif2 29937 subfacp1lem6 31709 erdszelem5 31719 pconnconn 31755 cvmseu 31800 neibastop2lem 32888 topdifinffinlem 33739 sstotbnd3 34116 brtrclfv2 38859 corcltrcl 38871 disjinfi 40187 |
Copyright terms: Public domain | W3C validator |