This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The difference, union, and intersection of two classes The union of two classes 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 ⊢ ( ( 𝐴 ∈ ( 𝐵 ∪ 𝐶 ) ∧ ¬ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 )