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 )