Metamath Proof Explorer

Theorem elunsn

Description: Elementhood to 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