Theorem uneqri

Description: Inference from membership to union. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	uneqri.1	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
Assertion	uneqri	⊢ ( 𝐴 ∪ 𝐵 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		uneqri.1	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
2		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
3	2 1	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
4	3	eqriv	⊢ ( 𝐴 ∪ 𝐵 ) = 𝐶