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 snex
 |-  { 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 )