Theorem elunnel1

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

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

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	orcanai	|- ( ( A e. ( B u. C ) /\ -. A e. B ) -> A e. C )