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	⊢ ( ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ¬ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶 ) )
2	1	biimpi	⊢ ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶 ) )
3	2	orcomd	⊢ ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ∈ 𝐶 ∨ 𝐴 ∈ 𝐵 ) )
4	3	orcanai	⊢ ( ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ¬ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )