const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const If_i : prop set set set const Repl : set (set set) set const Eps_i : (set prop) set const Empty : set term Sep = \x:set.\p:set prop.If_i (?y:set.y iIn x & p y) (Repl x \y:set.If_i (p y) y (Eps_i \z:set.z iIn x & p z)) Empty axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom xm: !P:prop.P | ~ P axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P lemma !x:set.!p:set prop.!y:set.!z:set.z iIn x -> y = If_i (p z) z (Eps_i \w:set.w iIn x & p w) -> p z -> y = z -> y iIn x & p y lemma !x:set.!p:set prop.!y:set.!z:set.(?w:set.w iIn x & p w) -> y = If_i (p z) z (Eps_i \w:set.w iIn x & p w) -> ~ p z -> y = Eps_i (\w:set.w iIn x & p w) -> y iIn x & p y var x:set var p:set prop var y:set hyp ?z:set.z iIn x & p z claim If_i (?z:set.z iIn x & p z) (Repl x \z:set.If_i (p z) z (Eps_i \w:set.w iIn x & p w)) Empty = Repl x (\z:set.If_i (p z) z (Eps_i \w:set.w iIn x & p w)) -> y iIn If_i (?z:set.z iIn x & p z) (Repl x \z:set.If_i (p z) z (Eps_i \w:set.w iIn x & p w)) Empty -> y iIn x & p y