Apply unknownprop_168889ac2767512e36c59c4d8bc32e41d805ce681fce6d41f1fc82bd258fd1a7 with
prim6 0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_TransSet with 0.
The subproof is completed by applying UnivOf_ZF_closed with 0.
Apply unknownprop_2d427e86e80080bca0cd1cdb7569c48ac3ebc7f720e53d0aef56ae9082c9d013 with
λ x0 . x0 ∈ prim6 0.
The subproof is completed by applying L0.