Axiom ax-L12 29

Description: Variable Substitution.

Note: '𝑥' cannot occur in '𝑡'.

Assertion

Ref	Expression
ax-L12	⊢ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))

Distinct variable group:   𝑡,𝑥

Detailed syntax breakdown of Axiom ax-L12

Step	Hyp	Ref	Expression
1		objvar-x	. . . 4 objvar 𝑥
2	1	term-obj 1	. . 3 term 𝑥
3		term-t	. . 3 term 𝑡
4	2, 3	wff-equals 6	. 2 wff 𝑥 = 𝑡
5		wff-ph	. . 3 wff 𝜑
6	4, 5	wff-imp 10	. . . 4 wff (𝑥 = 𝑡 → 𝜑)
7	6, 1	wff-forall 8	. . 3 wff ∀𝑥(𝑥 = 𝑡 → 𝜑)
8	5, 7	wff-imp 10	. 2 wff (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
9	4, 8	wff-imp 10	1 wff (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))

This axiom is referenced by:  exi-P6  718  lemma-L6.01a  724