iuneqconst

Description: Indexed union of identical classes. (Contributed by AV, 5-Mar-2024)

		Ref	Expression
	Hypothesis	iuneqconst.p	$⊢ x = X \to B = C$
	Assertion	iuneqconst	$⊢ (X \in A \land \forall x \in A B = C) \to ⋃_{x \in A} B = C$

Step	Hyp	Ref	Expression
1		iuneqconst.p	$⊢ x = X \to B = C$
2		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
3	1	eleq2d	$⊢ x = X \to (y \in B \leftrightarrow y \in C)$
4	3	rspcev	$⊢ (X \in A \land y \in C) \to \exists x \in A y \in B$
5	4	adantlr	$⊢ ((X \in A \land \forall x \in A B = C) \land y \in C) \to \exists x \in A y \in B$
6	5	ex	$⊢ (X \in A \land \forall x \in A B = C) \to (y \in C \to \exists x \in A y \in B)$
7		nfv	$⊢ Ⅎ x X \in A$
8		nfra1	$⊢ Ⅎ x \forall x \in A B = C$
9	7 8	nfan	$⊢ Ⅎ x (X \in A \land \forall x \in A B = C)$
10		nfv	$⊢ Ⅎ x y \in C$
11		rsp	$⊢ \forall x \in A B = C \to (x \in A \to B = C)$
12		eleq2	$⊢ B = C \to (y \in B \leftrightarrow y \in C)$
13	12	biimpd	$⊢ B = C \to (y \in B \to y \in C)$
14	11 13	syl6	$⊢ \forall x \in A B = C \to (x \in A \to (y \in B \to y \in C))$
15	14	adantl	$⊢ (X \in A \land \forall x \in A B = C) \to (x \in A \to (y \in B \to y \in C))$
16	9 10 15	rexlimd	$⊢ (X \in A \land \forall x \in A B = C) \to (\exists x \in A y \in B \to y \in C)$
17	6 16	impbid	$⊢ (X \in A \land \forall x \in A B = C) \to (y \in C \leftrightarrow \exists x \in A y \in B)$
18	2 17	bitr4id	$⊢ (X \in A \land \forall x \in A B = C) \to (y \in ⋃_{x \in A} B \leftrightarrow y \in C)$
19	18	eqrdv	$⊢ (X \in A \land \forall x \in A B = C) \to ⋃_{x \in A} B = C$

Metamath Proof Explorer