Supplement to Frege's Theorem and Foundations for Arithmetic
A More Complex Example
If given the premise that
1+22=5
one can prove that
1∈ϵ[λzz+22=5]
For it follows from our premise (by λ-Abstraction) that:
[λzz+22=5]1
Independently, by the logic of identity, we know:
ϵ[λzz+22=5]=ϵ[λzz+22=5]
So we may conjoin this fact and the result of λ-Abstraction to produce:
ϵ[λzz+22=5]=ϵ[λzz+22=5]&[λzz+22=5]1
Then, by existential generalization on the concept [λzz+22=5], it follows that:
∃G[ϵ[λzz+22=5]=ϵG&G1]
And, finally, by the definition of membership, we obtain:
1∈ϵ[λzz+22=5],
which is what we were trying to prove.