Theorem iuneq2

Description: Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003)

	Ref	Expression
Assertion	iuneq2	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ss2iun	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 )
2		ss2iun	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
3	1 2	anim12i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
4		eqss	⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) )
5	4	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) )
6		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) )
7	5 6	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ) )
8		eqss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
9	3 7 8	3imtr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 )