Axiom ax-aleq 333

Description: Quantified equality.

Assertion

Ref	Expression
ax-aleq	⊦ (~ x = y ⊸ (y = z ⊸ ∀x y = z))

Detailed syntax breakdown of Axiom ax-aleq

Step	Hyp	Ref	Expression
1		vx	. . . . 5 var x
2	1	nvar 203	. . . 4 nilad x
3		vy	. . . . 5 var y
4	3	nvar 203	. . . 4 nilad y
5	2, 4	weq 246	. . 3 wff x = y
6	5	wneg 3	. 2 wff ~ x = y
7		vz	. . . . 5 var z
8	7	nvar 203	. . . 4 nilad z
9	4, 8	weq 246	. . 3 wff y = z
10	9, 1	wal 318	. . 3 wff ∀x y = z
11	9, 10	wli 61	. 2 wff (y = z ⊸ ∀x y = z)
12	6, 11	wli 61	1 wff (~ x = y ⊸ (y = z ⊸ ∀x y = z))

This axiom is referenced by: (None)