proposition: Lemma range_inc_rw : forall f y, Function.axioms f -> inc y (range f) = (exists x, inc x (domain f) & y = V x f).
proof: Proof. ir. ap iff_eq; ir. cp (range_ex H H0). nin H1. sh x; xd. nin H0. ee. ap range_inc. am. sh x. xd. Qed.
imports: set_theory