Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23.

See exlimi for a more general version requiring more axioms.

This inference, along with its many variants such as [rexlimdv], is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf. In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element \( x \) exists satisfying a wff, i.e. E. x ph ( x ) where ph ( x ) has \( x \) free, then we can use ph ( C ) as a hypothesis for the proof where C is a new (fictitious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original \( \varphi \) (containing \( x \)) as an antecedent for the main part of the proof. We eventually arrive at \( \varphi \rightarrow \psi \) where \( \psi \) is the theorem to be proved and does not contain \( x \). Then we apply exlimiv to arrive at \( \exists x \, \varphi \rightarrow \psi \). Finally, we separately prove \( \exists x \, \varphi \) and detach it with modus ponens [ax-mp] to arrive at the final theorem \( \psi \), see exlimiiv. (Contributed by NM, 21-Jun-1993.) Remove dependencies on [ax-6] and [ax-8]. (Revised by Wolf Lammen, 4-Dec-2017.)