Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: ZF_closed x0. Apply ZF_closed_E with x0, ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0 leaving 2 subgoals. The subproof is completed by applying H0. Assume H1: Union_closed x0. Assume H2: Power_closed x0. Assume H3: Repl_closed x0. The subproof is completed by applying H1. ■