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 ∈ A ∧ ∀ x ∈ A B = C → ⋃ x ∈ A B = C

Proof

Step Hyp Ref Expression
1 iuneqconst.p ⊢ x = X → B = C
2 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
3 1 eleq2d ⊢ x = X → y ∈ B ↔ y ∈ C
4 3 rspcev ⊢ X ∈ A ∧ y ∈ C → ∃ x ∈ A y ∈ B
5 4 adantlr ⊢ X ∈ A ∧ ∀ x ∈ A B = C ∧ y ∈ C → ∃ x ∈ A y ∈ B
6 5 ex ⊢ X ∈ A ∧ ∀ x ∈ A B = C → y ∈ C → ∃ x ∈ A y ∈ B
7 nfv ⊢ Ⅎ x X ∈ A
8 nfra1 ⊢ Ⅎ x ∀ x ∈ A B = C
9 7 8 nfan ⊢ Ⅎ x X ∈ A ∧ ∀ x ∈ A B = C
10 nfv ⊢ Ⅎ x y ∈ C
11 rsp ⊢ ∀ x ∈ A B = C → x ∈ A → B = C
12 eleq2 ⊢ B = C → y ∈ B ↔ y ∈ C
13 12 biimpd ⊢ B = C → y ∈ B → y ∈ C
14 11 13 syl6 ⊢ ∀ x ∈ A B = C → x ∈ A → y ∈ B → y ∈ C
15 14 adantl ⊢ X ∈ A ∧ ∀ x ∈ A B = C → x ∈ A → y ∈ B → y ∈ C
16 9 10 15 rexlimd ⊢ X ∈ A ∧ ∀ x ∈ A B = C → ∃ x ∈ A y ∈ B → y ∈ C
17 6 16 impbid ⊢ X ∈ A ∧ ∀ x ∈ A B = C → y ∈ C ↔ ∃ x ∈ A y ∈ B
18 2 17 bitr4id ⊢ X ∈ A ∧ ∀ x ∈ A B = C → y ∈ ⋃ x ∈ A B ↔ y ∈ C
19 18 eqrdv ⊢ X ∈ A ∧ ∀ x ∈ A B = C → ⋃ x ∈ A B = C