Proof 01. 1 ⊢ univ U, hypo. 02. 2 ⊢ x ∈ U, hypo. 03. ⊢ x ∩ y ⊆ x, intersection_incl_left. 04. 1, 2 ⊢ x ∩ y ∈ U, univ_closed_subset 1 3 2. univ_closed_intersection. ⊢ univ U → x ∈ U → x ∩ y ∈ U, subj_intro_ii 4.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, subset.