Axiom ax-eleq1 328

Description: Left equality for binary predicate. This consumes the equality.

Assertion

Ref	Expression
ax-eleq1	⊦ (x = y ⊸ (x ∈ z ⊸ y ∈ z))

Detailed syntax breakdown of Axiom ax-eleq1

Step	Hyp	Ref	Expression
1		vx	. . . 4 var x
2	1	nvar 203	. . 3 nilad x
3		vy	. . . 4 var y
4	3	nvar 203	. . 3 nilad y
5	2, 4	weq 246	. 2 wff x = y
6		vz	. . . 4 var z
7	1, 6	wel 322	. . 3 wff x ∈ z
8	3, 6	wel 322	. . 3 wff y ∈ z
9	7, 8	wli 61	. 2 wff (x ∈ z ⊸ y ∈ z)
10	5, 9	wli 61	1 wff (x = y ⊸ (x ∈ z ⊸ y ∈ z))

This axiom is referenced by: (None)