Theorem ndalli-P7.17 842

Description: Natural Deduction: '∀' Introduction Rule.

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

'⊢ (𝛾 → 𝜑(𝑦))   ⇒   ⊢ (𝛾 → ∀𝑥𝜑(𝑥))',

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

The English interpetation of this rule is as follows -- if we can duduce '𝜑(𝑦)' for a specific, but *arbitrary*, '𝑦', then we can deduce that '𝜑(𝑥)' for *any* '𝑥'. To guarantee that '𝑦' is *arbitrary*, '𝑦' must not occur free in '𝛾' (the list of assumptions from which '𝜑(𝑦)' was deduced). Within a proof, the invocation of this rule is often indicated by the use of the phrase "without loss of generality".

Hypotheses

Ref	Expression
ndalli-P7.17.1	⊢ Ⅎ𝑦𝛾
ndalli-P7.17.2	⊢ Ⅎ𝑦𝜑
ndalli-P7.17.3	⊢ (𝛾 → [𝑦 / 𝑥]𝜑)

Assertion

Ref	Expression
ndalli-P7.17	⊢ (𝛾 → ∀𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Proof of Theorem ndalli-P7.17

Step	Hyp	Ref	Expression
1		ndalli-P7.17.1	. 2 ⊢ Ⅎ𝑦𝛾
2		ndalli-P7.17.2	. 2 ⊢ Ⅎ𝑦𝜑
3		ndalli-P7.17.3	. 2 ⊢ (𝛾 → [𝑦 / 𝑥]𝜑)
4	1, 2, 3	ndalli-P6 822	1 ⊢ (𝛾 → ∀𝑥𝜑)

Syntax hints:  term-obj 1  ∀wff-forall 8   → wff-imp 10  Ⅎ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:  ndalli-P7.17.VR1of2  864  ndalli-P7.17.VR2of2  865  ndalli-P7.17.VR12of2  866