Hello! This is pretty much my first venture in to this notation, and I was wondering if someone could help me with this: ∀x(Fx → ∀y(Fy → y=x)) As far as I am aware, ∀y(Fy → y=x) means for all y, whatever y you plug in, its domain is limited to x, so y is x, and f(y) is f(x): i.e. it limits y to 'being' x. Something like (Fx & ∀y(Fy → y=x)) makes sense, because its basically saying F can only be over x: there is only one F, namely x; if we tried to introduce something else, ∀y(Fy → y=x) tells us that it has to be x, so it can't be anything else, only x. If ∀y(Fy → y=x) = u then what does ∀x(Fx → u) mean? There's no u = x, is it over a domain?, or is it saying if F(x) is true then u? In which case the same notation is saying different things, which apparently it can; but in this case without clarification that this is is happening. Or is it saying something like: for all x: for F(x), y in F(y) is limited to being x, and that this is true for all y? Hopefully that makes sense. Any help appreciated!