Metamath Proof Explorer

Theorem uniel

Description: Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025)

Ref Expression
Assertion uniel ⊢ ⋃ A ∈ B ↔ ∃ x ∈ B ∀ z z ∈ x ↔ ∃ y ∈ A z ∈ y

Proof

Step Hyp Ref Expression
1 clabel ⊢ z | ∃ y ∈ A z ∈ y ∈ B ↔ ∃ x x ∈ B ∧ ∀ z z ∈ x ↔ ∃ y ∈ A z ∈ y
2 dfuni2 ⊢ ⋃ A = z | ∃ y ∈ A z ∈ y
3 2 eleq1i ⊢ ⋃ A ∈ B ↔ z | ∃ y ∈ A z ∈ y ∈ B
4 df-rex ⊢ ∃ x ∈ B ∀ z z ∈ x ↔ ∃ y ∈ A z ∈ y ↔ ∃ x x ∈ B ∧ ∀ z z ∈ x ↔ ∃ y ∈ A z ∈ y
5 1 3 4 3bitr4i ⊢ ⋃ A ∈ B ↔ ∃ x ∈ B ∀ z z ∈ x ↔ ∃ y ∈ A z ∈ y