family_union

Theorem family_union_intro

Theorem. family_union_intro
set (A i) → i ∈ I → x ∈ A i → x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i}

Proof
01. 1 ⊢ set (A i), hypo.
02. 2 ⊢ i ∈ I, hypo.
03. 3 ⊢ x ∈ A i, hypo.
04. ⊢ A i = A i, eq_refl.
05. 2 ⊢ i ∈ I ∧ A i = A i, conj_intro 2 4.
06. 2 ⊢ ∃j. j ∈ I ∧ A i = A j, ex_intro 5.
07. 1, 2 ⊢ A i ∈ {B | ∃j. j ∈ I ∧ B = A j},
  comp_intro 1 6, P u ↔ (∃j. j ∈ I ∧ u = A j).
08. 1, 2, 3 ⊢ x ∈ ⋃{B | ∃j. j ∈ I ∧ B = A j}, Union_intro 7 3.
family_union_intro. ⊢ set (A i) → i ∈ I → x ∈ A i →
  x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i}, subj_intro_iii 8.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.