Theorem uneq1

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	uneq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
2	1	orbi1d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) )
3		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) )
4		elun	⊢ ( 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) )
5	2 3 4	3bitr4g	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ↔ 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ) )
6	5	eqrdv	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) )