This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )