Supplement to Frege's Theorem and Foundations for Arithmetic
Proof of the Principle of Extensionality from Basic Law V
[Note: We use εF to denote the extension of the concept F.]
Assume Extension(x) and Extension(y). Then ∃F(x = εF) and ∃G(y = εG). Let P,Q be arbitrary such concepts; i.e., suppose x = εP and y = εQ.
Now to complete the proof, assume ∀z(z∈x ≡ z∈y). It then follows that ∀z(z ∈ εP ≡ z ∈ εQ). So, by the Law of Extensions and the principles of predicate logic, we may convert both conditions in the universalized biconditional to establish that ∀z(Pz ≡ Qz). So by Basic Law V, εP = εQ. So x = y.