Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply Eps_i_ex with
λ x2 . ∀ x3 . iff (prim1 x3 x2) (∃ x4 . and (prim1 x4 x0) (x3 = x1 x4)).
The subproof is completed by applying unknownprop_167865a0418480fa8f32a1c9d562a88fe56edc968c7a6cd028183a644298512b with x0, x1.