Axiom ax-L9-succ 22

Description: Successor substitution.

Assertion

Ref	Expression
ax-L9-succ	⊢ (𝑡 = 𝑢 → s‘𝑡 = s‘𝑢)

Detailed syntax breakdown of Axiom ax-L9-succ

Step	Hyp	Ref	Expression
1		term-t	. . 3 term 𝑡
2		term-u	. . 3 term 𝑢
3	1, 2	wff-equals 6	. 2 wff 𝑡 = 𝑢
4	1	term_succ 3	. . 3 term s‘𝑡
5	2	term_succ 3	. . 3 term s‘𝑢
6	4, 5	wff-equals 6	. 2 wff s‘𝑡 = s‘𝑢
7	3, 6	wff-imp 10	1 wff (𝑡 = 𝑢 → s‘𝑡 = s‘𝑢)

This axiom is referenced by:  subsucc-P5  644  nfrsucc-P6  780