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 )