Proof 01. 1 ⊢ x ∈ A ∩ UnivCl, hypo. 02. 1 ⊢ x ∈ A, intersection_eliml 1. 03. ⊢ x ∈ A ∩ UnivCl → x ∈ A, subj_intro 2. 04. 4 ⊢ x ∈ A, hypo. 05. 4 ⊢ set x, set_intro 4. 06. 4 ⊢ x ∈ UnivCl, UnivCl_intro 5. 07. 4 ⊢ x ∈ A ∩ UnivCl, intersection_intro 4 6. 08. ⊢ x ∈ A → x ∈ A ∩ UnivCl, subj_intro 7. 09. ⊢ x ∈ A ∩ UnivCl ↔ x ∈ A, bij_intro 3 8. 10. ⊢ ∀x. x ∈ A ∩ UnivCl ↔ x ∈ A, uq_intro 9. intersection_neutr. ⊢ A ∩ UnivCl = A, ext 10.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.