Metamath Proof Explorer

Theorem eliun

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion eliun ⊢ A ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B A ∈ C

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ ⋃ x ∈ B C → A ∈ V
2 elex ⊢ A ∈ C → A ∈ V
3 2 rexlimivw ⊢ ∃ x ∈ B A ∈ C → A ∈ V
4 eleq1 ⊢ y = A → y ∈ C ↔ A ∈ C
5 4 rexbidv ⊢ y = A → ∃ x ∈ B y ∈ C ↔ ∃ x ∈ B A ∈ C
6 df-iun ⊢ ⋃ x ∈ B C = y | ∃ x ∈ B y ∈ C
7 5 6 elab2g ⊢ A ∈ V → A ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B A ∈ C
8 1 3 7 pm5.21nii ⊢ A ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B A ∈ C