iuneqconst2

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

		Ref	Expression
	Assertion	iuneqconst2	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋃_{x \in A} B = C$

Step	Hyp	Ref	Expression
1		eqimss	$⊢ B = C \to B \subseteq C$
2	1	ralimi	$⊢ \forall x \in A B = C \to \forall x \in A B \subseteq C$
3	2	adantl	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to \forall x \in A B \subseteq C$
4		iunss	$⊢ ⋃_{x \in A} B \subseteq C \leftrightarrow \forall x \in A B \subseteq C$
5	3 4	sylibr	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋃_{x \in A} B \subseteq C$
6		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to \exists x \in A B = C$
7		eqimss2	$⊢ B = C \to C \subseteq B$
8	7	reximi	$⊢ \exists x \in A B = C \to \exists x \in A C \subseteq B$
9		ssiun	$⊢ \exists x \in A C \subseteq B \to C \subseteq ⋃_{x \in A} B$
10	6 8 9	3syl	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to C \subseteq ⋃_{x \in A} B$
11	5 10	eqssd	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋃_{x \in A} B = C$

Metamath Proof Explorer