Theorem ndexe-P7.20 845

Description: Natural Deduction: '∃' Elimination Rule.

In the traditional textbook presentation '[𝑦 / 𝑥]𝜑' and '𝜑' are written as '𝜑(𝑦)' and '𝜑(𝑥)', respectively. The rule is then stated as...

'⊢ (𝛾 → (𝜑(𝑦) → 𝜓))   &   ⊢ (𝛾 → ∃𝑥𝜑(𝑥))   ⇒   ⊢ (𝛾 → 𝜓)',

where '𝑦' cannot occur free in either '𝛾' or '𝜓' (that '𝑦' does not occur free in '𝜑(𝑥)' is implied by the notation).

The English interpretation of this rule is not as straighforward as the previous rules. In a typical proof, one will encounter a statement "let '𝑦' be a something such that '𝜑(𝑦)'" and then go on to deduce '𝜓' over several lines as a sub-proof. To be rigorous, the Deduction Theorem needs to be used to obtain '(𝜑(𝑦) → 𝜓)'. However, in most informal proofs the statement '(𝜑(𝑦) → 𝜓)' is omitted. Instead, the sub-proof is immediately preceeded by the statement that an '𝑥' such that '𝜑(𝑥)' has been shown to exist, invoking the second hypothesis. '𝜓' is then stated as the conclusion, immediately after the subproof. Typically, a sub-proof beginning with "let" is an indication that this rule will be used (at the conclusion of the sub-proof).

As for the non-freeness condition, that '𝑦' should not occur free in the context, '𝛾', is clear from the fact that '𝑦' is declared using the word "let", which indicates that '𝑦' is a new variable. That '𝑦' should not occur free in the conclusion '𝜓' is clear from the fact that this rule is used to discharch any statement referencing the temporary variable '𝑦'.

In metamath, to avoid using the Deduction Theorem, the assumptions necessary for the sub-proof are simply added to the context (list of assumptions on the left side of the sequent indicated by '𝛾'). This is where temporary variables normally associated with a "let" statement will appear. Such temporary variables are later discharged by invoking this rule.

One thing slightly different here is the the third non-freeness hypothesis. Only *conditional* non-freeness of '𝑦' in '𝜒', where '𝛾' is the condition, is necessary. This makes the rule slightly stronger than if we required the stronger hypothesis, '⊢ Ⅎ𝑦𝜓'. This slight strengthing seems to be necessary to deduce the closed form '(Ⅎ𝑥 → (𝜑 → ∀𝑥𝜑))'. The weaker form, given by ndexew-P7 867, is more typically used however.

Hypotheses

Ref	Expression
ndexe-P7.20.1	⊢ Ⅎ𝑦𝛾
ndexe-P7.20.2	⊢ Ⅎ𝑦𝜑
ndexe-P7.20.3	⊢ (𝛾 → Ⅎ𝑦𝜓)
ndexe-P7.20.4	⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))
ndexe-P7.20.5	⊢ (𝛾 → ∃𝑥𝜑)

Assertion

Ref	Expression
ndexe-P7.20	⊢ (𝛾 → 𝜓)

Distinct variable group:   𝑥,𝑦

Proof of Theorem ndexe-P7.20

Step	Hyp	Ref	Expression
1		ndexe-P7.20.1	. 2 ⊢ Ⅎ𝑦𝛾
2		ndexe-P7.20.2	. 2 ⊢ Ⅎ𝑦𝜑
3		ndexe-P7.20.3	. 2 ⊢ (𝛾 → Ⅎ𝑦𝜓)
4		ndexe-P7.20.4	. 2 ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))
5		ndexe-P7.20.5	. 2 ⊢ (𝛾 → ∃𝑥𝜑)
6	1, 2, 3, 4, 5	ndexe-P6 825	1 ⊢ (𝛾 → 𝜓)

Syntax hints:  term-obj 1   → wff-imp 10  ∃wff-exists 595  Ⅎwff-nfree 681  [wff-psub 714

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L10 27  ax-L11 28  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  ndexew-P7  867  lemma-L7.03  962