Metamath Proof Explorer

Theorem inelcm

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

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

Proof

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