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