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

Metamath Proof Explorer

Theorem iuneqconst2

Description: Indexed union of identical classes. (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Assertion iuneqconst2 ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 eqimss ⊢ ( 𝐵 = 𝐶 → 𝐵 ⊆ 𝐶 )
2 1 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
3 2 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
4 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
5 3 4 sylibr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
6 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )
7 eqimss2 ⊢ ( 𝐵 = 𝐶 → 𝐶 ⊆ 𝐵 )
8 7 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∃ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )
9 ssiun ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
10 6 8 9 3syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
11 5 10 eqssd ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )