 Extensionality of Functions: \(\forall X \forall Y \forall F[X \approx Y \rightarrow  FX = FY]\), where  \(X \approx Y\) is an abbreviation for \(\forall x[X(x) \leftrightarrow Y(x)]\), that is, \(X\) and \(Y\) are extensionally equivalent.