Proof
01. 1 ⊢ x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i}, hypo.
02. 1 ⊢ ∃B. B ∈ {B | ∃i. i ∈ I ∧ B = A i} ∧ x ∈ B, Union_elim 1.
03. 3 ⊢ B ∈ {B | ∃i. i ∈ I ∧ B = A i} ∧ x ∈ B, hypo.
04. 3 ⊢ B ∈ {B | ∃i. i ∈ I ∧ B = A i}, conj_eliml 3.
05. 3 ⊢ ∃i. i ∈ I ∧ B = A i, comp_elim 4.
06. 6 ⊢ i ∈ I ∧ B = A i, hypo.
07. 6 ⊢ i ∈ I, conj_eliml 6.
08. 6 ⊢ B = A i, conj_elimr 6.
09. 3 ⊢ x ∈ B, conj_elimr 3.
10. 3, 6 ⊢ x ∈ A i, eq_subst 8 9, P u ↔ x ∈ u.
11. 3 ⊢ set B, set_intro 4.
12. 3, 6 ⊢ set (A i), eq_subst 8 11.
13. 3, 6 ⊢ i ∈ I ∧ x ∈ A i, conj_intro 7 10.
14. 3, 6 ⊢ i ∈ I ∧ x ∈ A i ∧ set (A i), conj_intro 13 12.
15. 3, 6 ⊢ ∃i. i ∈ I ∧ x ∈ A i ∧ set (A i), ex_intro 14.
16. 3 ⊢ ∃i. i ∈ I ∧ x ∈ A i ∧ set (A i), ex_elim 5 15.
17. 1 ⊢ ∃i. i ∈ I ∧ x ∈ A i ∧ set (A i), ex_elim 2 16.
family_union_elim. ⊢ x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i} →
∃i. i ∈ I ∧ x ∈ A i ∧ set (A i), subj_intro 17.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.