This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rext

Description: A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of TakeutiZaring p. 16. (Contributed by NM, 10-Aug-1993)

Ref Expression
Assertion rext ⊢ ∀ z x ∈ z → y ∈ z → x = y

Proof

Step Hyp Ref Expression
1 vsnid ⊢ x ∈ x
2 vsnex ⊢ x ∈ V
3 eleq2 ⊢ z = x → x ∈ z ↔ x ∈ x
4 eleq2 ⊢ z = x → y ∈ z ↔ y ∈ x
5 3 4 imbi12d ⊢ z = x → x ∈ z → y ∈ z ↔ x ∈ x → y ∈ x
6 2 5 spcv ⊢ ∀ z x ∈ z → y ∈ z → x ∈ x → y ∈ x
7 1 6 mpi ⊢ ∀ z x ∈ z → y ∈ z → y ∈ x
8 velsn ⊢ y ∈ x ↔ y = x
9 equcomi ⊢ y = x → x = y
10 8 9 sylbi ⊢ y ∈ x → x = y
11 7 10 syl ⊢ ∀ z x ∈ z → y ∈ z → x = y