Axiom ax-eleq2 329

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

Assertion

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

Detailed syntax breakdown of Axiom ax-eleq2

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	6, 1	wel 322	. . 3 wff z ∈ x
8	6, 3	wel 322	. . 3 wff z ∈ y
9	7, 8	wli 61	. 2 wff (z ∈ x ⊸ z ∈ y)
10	5, 9	wli 61	1 wff (x = y ⊸ (z ∈ x ⊸ z ∈ y))

This axiom is referenced by: (None)