Theorem elunsn

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

	Ref	Expression
Assertion	elunsn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝐴 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐶 } ) )
2		elsng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐶 } ↔ 𝐴 = 𝐶 ) )
3	2	orbi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶 ) ) )
4	1 3	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶 ) ) )