Lawvere's fixed point theorem states that that in a cartesian closed category, if there is a morphism $ϕ: A \to B^A$ which is point-surjective (i.e., for every point $q : 1 \to B^A$ there exists a point $p : 1 \to A$ such that $ϕp = q$), then every endomorphism $f : B \to B$ has a fixed point.
The fixed point of $f$ is obtained as $ϕ(p)(p)$ where $p : 1 \to A$ is the point of $A$ such that $ϕp = q$ for $q : 1 \to B^A$ defined in lambda calculus notation as $q = λa:A.fϕ(a)(a)$.
I've seen it remarked several times that the existence of Y combinator in lambda calculus, i.e., $Y = λf.(λx.f(xx))(λx.f(xx))$, is an application of Lawvere's fixed point theorem, but the remark has always been made only in passing and I haven't been able to figure out precisely how to get from the one to the other.
Can someone help me out by making the application explicit?