# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({X}\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\right)\to \bigcup _{{x}\in {A}}{B}={C}$

### Proof

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