Metamath Proof Explorer
Description: A member of a union that is not member of the first class, is member of
the second class. (Contributed by Glauco Siliprandi, 11Dec2019)


Ref 
Expression 

Assertion 
elunnel1 
⊢ ( ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ¬ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

elun 
⊢ ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶 ) ) 
2 
1

biimpi 
⊢ ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶 ) ) 
3 
2

orcanai 
⊢ ( ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ¬ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 ) 