Proof 01. ⊢ (∃C. x ∈ C) → set x, bij_elimr set_equi. 02. 2 ⊢ x ∈ A, hypo. 03. 2 ⊢ ∃C. x ∈ C, ex_intro 2. 04. 2 ⊢ set x, subj_elim 1 3. set_intro. ⊢ x ∈ A → set x, subj_intro 4.