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 
|- ( A. z ( x e. z -> y e. z ) -> x = y )

Proof

Step Hyp Ref Expression
1 vsnid 
 |-  x e. { x }
2 vsnex 
 |-  { x } e. _V
3 eleq2 
 |-  ( z = { x } -> ( x e. z <-> x e. { x } ) )
4 eleq2 
 |-  ( z = { x } -> ( y e. z <-> y e. { x } ) )
5 3 4 imbi12d 
 |-  ( z = { x } -> ( ( x e. z -> y e. z ) <-> ( x e. { x } -> y e. { x } ) ) )
6 2 5 spcv 
 |-  ( A. z ( x e. z -> y e. z ) -> ( x e. { x } -> y e. { x } ) )
7 1 6 mpi 
 |-  ( A. z ( x e. z -> y e. z ) -> y e. { x } )
8 velsn 
 |-  ( y e. { x } <-> y = x )
9 equcomi 
 |-  ( y = x -> x = y )
10 8 9 sylbi 
 |-  ( y e. { x } -> x = y )
11 7 10 syl 
 |-  ( A. z ( x e. z -> y e. z ) -> x = y )