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∈AB∈C→⋃x∈AB=⋃y|∃x∈Ay=B

Proof

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