![]() |
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 3897 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
2 | ne0i 4250 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | |
3 | 1, 2 | sylbir 238 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ≠ wne 2987 ∩ cin 3880 ∅c0 4243 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-dif 3884 df-in 3888 df-nul 4244 |
This theorem is referenced by: minel 4373 disji 5013 disjiun 5017 onnseq 7964 uniinqs 8360 en3lplem1 9059 cplem1 9302 fpwwe2lem12 10052 limsupgre 14830 lmcls 21907 conncn 22031 iunconnlem 22032 conncompclo 22040 2ndcsep 22064 lfinpfin 22129 locfincmp 22131 txcls 22209 pthaus 22243 qtopeu 22321 trfbas2 22448 filss 22458 zfbas 22501 fmfnfm 22563 tsmsfbas 22733 restmetu 23177 qdensere 23375 reperflem 23423 reconnlem1 23431 metds0 23455 metnrmlem1a 23463 minveclem3b 24032 ovolicc2lem5 24125 taylfval 24954 wlk1walk 27428 wwlksm1edg 27667 disjif 30341 disjif2 30344 subfacp1lem6 32545 erdszelem5 32555 pconnconn 32591 cvmseu 32636 neibastop2lem 33821 topdifinffinlem 34764 sstotbnd3 35214 brtrclfv2 40428 corcltrcl 40440 disjinfi 41820 |
Copyright terms: Public domain | W3C validator |