 For the purposes of understanding Frege’s Theorem, we only need to introduce one axiom that governs \(\lambda\)-notation, namely, the principle known as \(\lambda \)-Conversion. Let \(\phi\) be any formula and let \(\phi^y_x\) be the result of substituting the variable \(y\) for free occurrences of \(x\) everywhere in \(\phi\). Then the principle of \(\lambda\)-Conversion is: