const Eps_i : (set prop) set term If_i = \P:prop.\x:set.\y:set.Eps_i \z:set.P & z = x | ~ P & z = y axiom Eps_i_ax: !p:set prop.!x:set.p x -> p (Eps_i p) var P:prop var x:set var y:set hyp ~ P claim P & y = x | ~ P & y = y -> P & Eps_i (\z:set.P & z = x | ~ P & z = y) = x | ~ P & Eps_i (\z:set.P & z = x | ~ P & z = y) = y