Theorem iuneqconst

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

	Ref	Expression
Hypothesis	iuneqconst.p	|- ( x = X -> B = C )
Assertion	iuneqconst	|- ( ( X e. A /\ A. x e. A B = C ) -> U_ x e. A B = C )

Proof

Step	Hyp	Ref	Expression
1		iuneqconst.p	|- ( x = X -> B = C )
2		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
3	1	eleq2d	|- ( x = X -> ( y e. B <-> y e. C ) )
4	3	rspcev	|- ( ( X e. A /\ y e. C ) -> E. x e. A y e. B )
5	4	adantlr	|- ( ( ( X e. A /\ A. x e. A B = C ) /\ y e. C ) -> E. x e. A y e. B )
6	5	ex	|- ( ( X e. A /\ A. x e. A B = C ) -> ( y e. C -> E. x e. A y e. B ) )
7		nfv	|- F/ x X e. A
8		nfra1	|- F/ x A. x e. A B = C
9	7 8	nfan	|- F/ x ( X e. A /\ A. x e. A B = C )
10		nfv	|- F/ x y e. C
11		rsp	|- ( A. x e. A B = C -> ( x e. A -> B = C ) )
12		eleq2	|- ( B = C -> ( y e. B <-> y e. C ) )
13	12	biimpd	|- ( B = C -> ( y e. B -> y e. C ) )
14	11 13	syl6	|- ( A. x e. A B = C -> ( x e. A -> ( y e. B -> y e. C ) ) )
15	14	adantl	|- ( ( X e. A /\ A. x e. A B = C ) -> ( x e. A -> ( y e. B -> y e. C ) ) )
16	9 10 15	rexlimd	|- ( ( X e. A /\ A. x e. A B = C ) -> ( E. x e. A y e. B -> y e. C ) )
17	6 16	impbid	|- ( ( X e. A /\ A. x e. A B = C ) -> ( y e. C <-> E. x e. A y e. B ) )
18	2 17	bitr4id	|- ( ( X e. A /\ A. x e. A B = C ) -> ( y e. U_ x e. A B <-> y e. C ) )
19	18	eqrdv	|- ( ( X e. A /\ A. x e. A B = C ) -> U_ x e. A B = C )