Proof 01. 1 ⊢ univ U, hypo. 02. 2 ⊢ x ∈ U, hypo. 03. 1, 2 ⊢ x ⊆ U, univ_trans 1 2. 04. 2 ⊢ set x, set_intro 2. 05. 1, 2 ⊢ x ∈ power U, power_intro 4 3. 06. 1 ⊢ x ∈ U → x ∈ power U, subj_intro 5. 07. 1 ⊢ ∀x. x ∈ U → x ∈ power U, uq_intro 6. 08. 1 ⊢ U ⊆ power U, incl_intro 7. 09. 1 ⊢ U ∩ power U = U, intersection_from_incl 8. truncated_power_idem. ⊢ univ U → U ∩ power U = U, subj_intro 9.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.