Theorem iuneqconst2

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

	Ref	Expression
Assertion	iuneqconst2	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to \bigcup _{x\in A}B=C$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢B=C\to B\subseteq C$$
2	1	ralimi	$$⊢\forall x\in AB=C\to \forall x\in AB\subseteq C$$
3	2	adantl	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to \forall x\in AB\subseteq C$$
4		iunss	$$⊢\bigcup _{x\in A}B\subseteq C\leftrightarrow \forall x\in AB\subseteq C$$
5	3 4	sylibr	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to \bigcup _{x\in A}B\subseteq C$$
6		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to \exists x\in AB=C$$
7		eqimss2	$$⊢B=C\to C\subseteq B$$
8	7	reximi	$$⊢\exists x\in AB=C\to \exists x\in AC\subseteq B$$
9		ssiun	$$⊢\exists x\in AC\subseteq B\to C\subseteq \bigcup _{x\in A}B$$
10	6 8 9	3syl	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to C\subseteq \bigcup _{x\in A}B$$
11	5 10	eqssd	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB=C\right)\to \bigcup _{x\in A}B=C$$