Metamath Proof Explorer

Theorem dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Assertion dfiun2g ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ∈ C
2 rspa ⊢ ∀ x ∈ A B ∈ C ∧ x ∈ A → B ∈ C
3 clel3g ⊢ B ∈ C → z ∈ B ↔ ∃ y y = B ∧ z ∈ y
4 2 3 syl ⊢ ∀ x ∈ A B ∈ C ∧ x ∈ A → z ∈ B ↔ ∃ y y = B ∧ z ∈ y
5 1 4 rexbida ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ x ∈ A ∃ y y = B ∧ z ∈ y
6 rexcom4 ⊢ ∃ x ∈ A ∃ y y = B ∧ z ∈ y ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
7 5 6 bitrdi ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
8 r19.41v ⊢ ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ x ∈ A y = B ∧ z ∈ y
9 8 exbii ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
10 exancom ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
11 9 10 bitri ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
12 7 11 bitrdi ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
13 eliun ⊢ z ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A z ∈ B
14 eluniab ⊢ z ∈ ⋃ y | ∃ x ∈ A y = B ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
15 12 13 14 3bitr4g ⊢ ∀ x ∈ A B ∈ C → z ∈ ⋃ x ∈ A B ↔ z ∈ ⋃ y | ∃ x ∈ A y = B
16 15 eqrdv ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B