Content deleted Content added
Line 146:
of functional predicates which are not sets makes it useful to allow the notation F(x)
both for sets F and for important functional predicates. As long as one does not quantify
over functions in the latter sense, all such uses are in principle eliminable. For any set A,
we define <math>F``A</math> as <math>\{y \mid (\exists x.x \in A \wedge y=F(x))\}</math>,
more conveniently written as <math>\{F(x) \mid x \in A\}</math>. If A is a set and F
is any functional relation, <math>F``A</math> is a set in [[ZFC]] by Replacement. In [[NFU]],
notice that in <math}F(x)</math>, x has the same type as the expression, and F is three
types higher (one type higher if a type-level pair is used).
The function I defined by I(x) = x does not exist as a set in [[ZFC]] because it is "too large"
| |||