Theorem inelcm 4421

Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)

Assertion

Ref	Expression
inelcm	⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)

Proof of Theorem inelcm

Step	Hyp	Ref	Expression
1		elin 4096	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2		ne0i 4290	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
3	1, 2	sylbir 238	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2959   ∩ cin 4092  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  minel  4422  disji  5091  disjiun  5094  onnseq  8366  uniinqs  8832  en3lplem1  9626  cplem1  9963  cplem1OLD  9964  fpwwe2lem11  10739  limsupgre  15663  cat1lem  18286  lmcls  23635  conncn  23759  iunconnlem  23760  conncompclo  23768  2ndcsep  23793  lfinpfin  23858  locfincmp  23860  txcls  23938  pthaus  23972  qtopeu  24050  trfbas2  24177  filss  24187  zfbas  24230  fmfnfm  24292  tsmsfbas  24462  restmetu  24904  qdensere  25103  reperflem  25153  reconnlem1  25161  metds0  25185  metnrmlem1a  25193  minveclem3b  25764  ovolicc2lem5  25857  taylfval  26701  prlnghpg  29439  wlk1walk  30234  wwlksm1edg  30485  disjif  33229  disjif2  33232  dfufd2lem  34137  subfacp1lem6  36074  erdszelem5  36084  pconnconn  36120  cvmseu  36165  neibastop2lem  37281  topdifinffinlem  38416  sstotbnd3  38856  brtrclfv2  44873  corcltrcl  44885  disjinfi  46352