Metamath Proof Explorer

Theorem dfiun2gOLD

Description: Obsolete version of dfiun2g as of 11-Dec-2024. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion dfiun2gOLD ⊢∀x∈AB∈C→⋃x∈AB=⋃y|∃x∈Ay=B

Proof

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