Theorem inelcm 2368

Description: The intersection of classes with a common member is nonempty.

Assertion

Ref	Expression
inelcm	|- ((A e. B /\ A e. C) -> (B i^i C) =/= (/))

Proof of Theorem inelcm

Step	Hyp	Ref	Expression
1		elin 2251	. 2 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))
2		ne0i 2330	. 2 |- (A e. (B i^i C) -> (B i^i C) =/= (/))
3	1, 2	sylbir 199	1 |- ((A e. B /\ A e. C) -> (B i^i C) =/= (/))

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 990   =/= wne 1622   i^i cin 2090  (/)c0 2324

This theorem is referenced by:  minel 2369  fr2nr 2980  fr3nr 2981  cplem1 4806  metelcls 8085  uninqs 10563  uninqsOLD 10564

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-in 2095  df-nul 2325

Copyright terms: Public domain