iuneq1i

Description: Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021) Remove DV conditions. (Revised by GG, 1-Sep-2025)

		Ref	Expression
	Hypothesis	iuneq1i.1	$⊢ A = B$
	Assertion	iuneq1i	$⊢ ⋃_{x \in A} C = ⋃_{x \in B} C$

Step	Hyp	Ref	Expression
1		iuneq1i.1	$⊢ A = B$
2	1	eleq2i	$⊢ x \in A \leftrightarrow x \in B$
3	2	anbi1i	$⊢ (x \in A \land t \in C) \leftrightarrow (x \in B \land t \in C)$
4	3	rexbii2	$⊢ \exists x \in A t \in C \leftrightarrow \exists x \in B t \in C$
5	4	abbii	$⊢ \{t \| \exists x \in A t \in C\} = \{t \| \exists x \in B t \in C\}$
6		df-iun	$⊢ ⋃_{x \in A} C = \{t \| \exists x \in A t \in C\}$
7		df-iun	$⊢ ⋃_{x \in B} C = \{t \| \exists x \in B t \in C\}$
8	5 6 7	3eqtr4i	$⊢ ⋃_{x \in A} C = ⋃_{x \in B} C$

Metamath Proof Explorer