![]() |
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 3963 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
2 | ne0i 4337 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | |
3 | 1, 2 | sylbir 234 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 ≠ wne 2930 ∩ cin 3946 ∅c0 4325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-v 3464 df-dif 3950 df-in 3954 df-nul 4326 |
This theorem is referenced by: minel 4470 disji 5136 disjiun 5140 onnseq 8374 uniinqs 8826 en3lplem1 9655 cplem1 9932 fpwwe2lem11 10684 limsupgre 15483 cat1lem 18118 lmcls 23297 conncn 23421 iunconnlem 23422 conncompclo 23430 2ndcsep 23454 lfinpfin 23519 locfincmp 23521 txcls 23599 pthaus 23633 qtopeu 23711 trfbas2 23838 filss 23848 zfbas 23891 fmfnfm 23953 tsmsfbas 24123 restmetu 24570 qdensere 24777 reperflem 24825 reconnlem1 24833 metds0 24857 metnrmlem1a 24865 minveclem3b 25447 ovolicc2lem5 25541 taylfval 26386 wlk1walk 29576 wwlksm1edg 29815 disjif 32498 disjif2 32501 dfufd2lem 33424 subfacp1lem6 35013 erdszelem5 35023 pconnconn 35059 cvmseu 35104 neibastop2lem 36072 topdifinffinlem 37054 sstotbnd3 37477 brtrclfv2 43394 corcltrcl 43406 disjinfi 44799 |
Copyright terms: Public domain | W3C validator |