Metamath Proof Explorer

Theorem elunsn

Description: Elementhood in a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023)

Ref Expression
Assertion elunsn ⊢ A ∈ V → A ∈ B ∪ C ↔ A ∈ B ∨ A = C

Proof

Step Hyp Ref Expression
1 elun ⊢ A ∈ B ∪ C ↔ A ∈ B ∨ A ∈ C
2 elsng ⊢ A ∈ V → A ∈ C ↔ A = C
3 2 orbi2d ⊢ A ∈ V → A ∈ B ∨ A ∈ C ↔ A ∈ B ∨ A = C
4 1 3 bitrid ⊢ A ∈ V → A ∈ B ∪ C ↔ A ∈ B ∨ A = C