Metamath Proof Explorer


Theorem elunnel2

Description: A member of a union that is not a member of the second class, is a member of the first class. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion elunnel2
|- ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B )

Proof

Step Hyp Ref Expression
1 elun
 |-  ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )
2 1 biimpi
 |-  ( A e. ( B u. C ) -> ( A e. B \/ A e. C ) )
3 2 orcomd
 |-  ( A e. ( B u. C ) -> ( A e. C \/ A e. B ) )
4 3 orcanai
 |-  ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B )