Description: 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'sA 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 ph (containing x ) as an antecedent for the main part of the proof. We eventually arrive at ( ph -> ps ) where ps is the theorem to be proved and does not contain x . Then we apply exlimiv to arrive at ( E. x ph -> ps ) . Finally, we separately prove E. x ph and detach it with modus ponens ax-mp to arrive at the final theorem ps , see exlimiiv . (Contributed by NM, 21-Jun-1993) Remove dependencies on ax-6 and ax-8 . (Revised by Wolf Lammen, 4-Dec-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | exlimiv.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| Assertion | exlimiv | ⊢ ( ∃ 𝑥 𝜑 → 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exlimiv.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| 2 | 1 | eximi | ⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) |
| 3 | ax5e | ⊢ ( ∃ 𝑥 𝜓 → 𝜓 ) | |
| 4 | 2 3 | syl | ⊢ ( ∃ 𝑥 𝜑 → 𝜓 ) |