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) Avoid ax-10 , ax-12 . (Revised by SN, 11-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = z | ∃ x ∈ A z ∈ B
2 elisset ⊢ B ∈ C → ∃ z z = B
3 eleq2 ⊢ z = B → w ∈ z ↔ w ∈ B
4 3 pm5.32ri ⊢ w ∈ z ∧ z = B ↔ w ∈ B ∧ z = B
5 4 simplbi2 ⊢ w ∈ B → z = B → w ∈ z ∧ z = B
6 5 eximdv ⊢ w ∈ B → ∃ z z = B → ∃ z w ∈ z ∧ z = B
7 2 6 syl5com ⊢ B ∈ C → w ∈ B → ∃ z w ∈ z ∧ z = B
8 7 ralimi ⊢ ∀ x ∈ A B ∈ C → ∀ x ∈ A w ∈ B → ∃ z w ∈ z ∧ z = B
9 rexim ⊢ ∀ x ∈ A w ∈ B → ∃ z w ∈ z ∧ z = B → ∃ x ∈ A w ∈ B → ∃ x ∈ A ∃ z w ∈ z ∧ z = B
10 8 9 syl ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A w ∈ B → ∃ x ∈ A ∃ z w ∈ z ∧ z = B
11 rexcom4 ⊢ ∃ x ∈ A ∃ z w ∈ z ∧ z = B ↔ ∃ z ∃ x ∈ A w ∈ z ∧ z = B
12 r19.42v ⊢ ∃ x ∈ A w ∈ z ∧ z = B ↔ w ∈ z ∧ ∃ x ∈ A z = B
13 12 exbii ⊢ ∃ z ∃ x ∈ A w ∈ z ∧ z = B ↔ ∃ z w ∈ z ∧ ∃ x ∈ A z = B
14 11 13 bitri ⊢ ∃ x ∈ A ∃ z w ∈ z ∧ z = B ↔ ∃ z w ∈ z ∧ ∃ x ∈ A z = B
15 10 14 imbitrdi ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A w ∈ B → ∃ z w ∈ z ∧ ∃ x ∈ A z = B
16 3 biimpac ⊢ w ∈ z ∧ z = B → w ∈ B
17 16 reximi ⊢ ∃ x ∈ A w ∈ z ∧ z = B → ∃ x ∈ A w ∈ B
18 12 17 sylbir ⊢ w ∈ z ∧ ∃ x ∈ A z = B → ∃ x ∈ A w ∈ B
19 18 exlimiv ⊢ ∃ z w ∈ z ∧ ∃ x ∈ A z = B → ∃ x ∈ A w ∈ B
20 15 19 impbid1 ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A w ∈ B ↔ ∃ z w ∈ z ∧ ∃ x ∈ A z = B
21 vex ⊢ w ∈ V
22 eleq1w ⊢ z = w → z ∈ B ↔ w ∈ B
23 22 rexbidv ⊢ z = w → ∃ x ∈ A z ∈ B ↔ ∃ x ∈ A w ∈ B
24 21 23 elab ⊢ w ∈ z | ∃ x ∈ A z ∈ B ↔ ∃ x ∈ A w ∈ B
25 eluni ⊢ w ∈ ⋃ y | ∃ x ∈ A y = B ↔ ∃ z w ∈ z ∧ z ∈ y | ∃ x ∈ A y = B
26 vex ⊢ z ∈ V
27 eqeq1 ⊢ y = z → y = B ↔ z = B
28 27 rexbidv ⊢ y = z → ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
29 26 28 elab ⊢ z ∈ y | ∃ x ∈ A y = B ↔ ∃ x ∈ A z = B
30 29 anbi2i ⊢ w ∈ z ∧ z ∈ y | ∃ x ∈ A y = B ↔ w ∈ z ∧ ∃ x ∈ A z = B
31 30 exbii ⊢ ∃ z w ∈ z ∧ z ∈ y | ∃ x ∈ A y = B ↔ ∃ z w ∈ z ∧ ∃ x ∈ A z = B
32 25 31 bitri ⊢ w ∈ ⋃ y | ∃ x ∈ A y = B ↔ ∃ z w ∈ z ∧ ∃ x ∈ A z = B
33 20 24 32 3bitr4g ⊢ ∀ x ∈ A B ∈ C → w ∈ z | ∃ x ∈ A z ∈ B ↔ w ∈ ⋃ y | ∃ x ∈ A y = B
34 33 eqrdv ⊢ ∀ x ∈ A B ∈ C → z | ∃ x ∈ A z ∈ B = ⋃ y | ∃ x ∈ A y = B
35 1 34 eqtrid ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B