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

Proof

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