Apply unknownprop_e747e5ba1c4c5fc029f52d44d14d3be2d06759ee5e8f12e8b1e65810154eb535 with
prim6 (prim6 0),
prim6 0 leaving 3 subgoals.
The subproof is completed by applying UnivOf_TransSet with
prim6 0.
The subproof is completed by applying UnivOf_ZF_closed with
prim6 0.
The subproof is completed by applying UnivOf_In with
prim6 0.
Apply unknownprop_31dcb8d5525508863c1b21cc955e4d494ebb1701faf26ee1ff3607fb19489de7 with
λ x0 . x0 ∈ prim6 (prim6 0).
The subproof is completed by applying L0.