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 1 eleq2d ⊢ x = X → y ∈ B ↔ y ∈ C
3 2 rspcev ⊢ X ∈ A ∧ y ∈ C → ∃ x ∈ A y ∈ B
4 3 adantlr ⊢ X ∈ A ∧ ∀ x ∈ A B = C ∧ y ∈ C → ∃ x ∈ A y ∈ B
5 4 ex ⊢ X ∈ A ∧ ∀ x ∈ A B = C → y ∈ C → ∃ x ∈ A y ∈ B
6 nfv ⊢ Ⅎ x X ∈ A
7 nfra1 ⊢ Ⅎ x ∀ x ∈ A B = C
8 6 7 nfan ⊢ Ⅎ x X ∈ A ∧ ∀ x ∈ A B = C
9 nfv ⊢ Ⅎ x y ∈ C
10 rsp ⊢ ∀ x ∈ A B = C → x ∈ A → B = C
11 eleq2 ⊢ B = C → y ∈ B ↔ y ∈ C
12 11 biimpd ⊢ B = C → y ∈ B → y ∈ C
13 10 12 syl6 ⊢ ∀ x ∈ A B = C → x ∈ A → y ∈ B → y ∈ C
14 13 adantl ⊢ X ∈ A ∧ ∀ x ∈ A B = C → x ∈ A → y ∈ B → y ∈ C
15 8 9 14 rexlimd ⊢ X ∈ A ∧ ∀ x ∈ A B = C → ∃ x ∈ A y ∈ B → y ∈ C
16 5 15 impbid ⊢ X ∈ A ∧ ∀ x ∈ A B = C → y ∈ C ↔ ∃ x ∈ A y ∈ B
17 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
18 16 17 syl6rbbr ⊢ 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