  The inferences which start with the premise ‘John loves Mary’, displayed above, both appeal to this axiom for justification. This axiom is actually derivable as a theorem from Frege’s Basic Law IIa (1893, §47). Basic Law IIa is formulated as \(\forall x\phi (x) \to \phi (a)\), where \(\phi(a)\) is the result of substituting \(a\) for one or more variables \(x\) bound by the quantifier (though see below for a more careful discussion of this axiom). So the axiom displayed above for the existential quantifier can be derived from IIa using the rules governing conditionals, negation, and the definition of \(\exists x\phi\) discussed above. 