Metamath Proof Explorer

Theorem dfiun2gOLD

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

Ref Expression
Assertion dfiun2gOLD ⊢ ∀ 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 rsp ⊢ ∀ x ∈ A B ∈ C → x ∈ A → B ∈ C
3 clel3g ⊢ B ∈ C → z ∈ B ↔ ∃ y y = B ∧ z ∈ y
4 2 3 syl6 ⊢ ∀ x ∈ A B ∈ C → x ∈ A → z ∈ B ↔ ∃ y y = B ∧ z ∈ y
5 4 imp ⊢ ∀ x ∈ A B ∈ C ∧ x ∈ A → z ∈ B ↔ ∃ y y = B ∧ z ∈ y
6 1 5 rexbida ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ x ∈ A ∃ y y = B ∧ z ∈ y
7 rexcom4 ⊢ ∃ x ∈ A ∃ y y = B ∧ z ∈ y ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
8 6 7 syl6bb ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
9 r19.41v ⊢ ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ x ∈ A y = B ∧ z ∈ y
10 9 exbii ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ y
11 exancom ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
12 10 11 bitri ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ y ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
13 8 12 syl6bb ⊢ ∀ x ∈ A B ∈ C → ∃ x ∈ A z ∈ B ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
14 eliun ⊢ z ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A z ∈ B
15 eluniab ⊢ z ∈ ⋃ y | ∃ x ∈ A y = B ↔ ∃ y z ∈ y ∧ ∃ x ∈ A y = B
16 13 14 15 3bitr4g ⊢ ∀ x ∈ A B ∈ C → z ∈ ⋃ x ∈ A B ↔ z ∈ ⋃ y | ∃ x ∈ A y = B
17 16 eqrdv ⊢ ∀ x ∈ A B ∈ C → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B