This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 )