const In : set set prop term iIn = In infix iIn 2000 2000 const Repl : set (set set) set term Repl_closed = \x:set.!y:set.y iIn x -> !f:set set.(!z:set.z iIn y -> f z iIn x) -> Repl y f iIn x const ZF_closed : set prop const Union_closed : set prop const Power_closed : set prop axiom ZF_closed_E: !x:set.ZF_closed x -> !P:prop.(Union_closed x -> Power_closed x -> Repl_closed x -> P) -> P claim !x:set.ZF_closed x -> !y:set.y iIn x -> !f:set set.(!z:set.z iIn y -> f z iIn x) -> Repl y f iIn x