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	$$⊢\forall z\left(x\in z\to y\in z\right)\to x=y$$

Proof

Step	Hyp	Ref	Expression
1		vsnid	$$⊢x\in \left\{x\right\}$$
2		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
3		eleq2	$$⊢z=\left\{x\right\}\to \left(x\in z\leftrightarrow x\in \left\{x\right\}\right)$$
4		eleq2	$$⊢z=\left\{x\right\}\to \left(y\in z\leftrightarrow y\in \left\{x\right\}\right)$$
5	3 4	imbi12d	$$⊢z=\left\{x\right\}\to \left(\left(x\in z\to y\in z\right)\leftrightarrow \left(x\in \left\{x\right\}\to y\in \left\{x\right\}\right)\right)$$
6	2 5	spcv	$$⊢\forall z\left(x\in z\to y\in z\right)\to \left(x\in \left\{x\right\}\to y\in \left\{x\right\}\right)$$
7	1 6	mpi	$$⊢\forall z\left(x\in z\to y\in z\right)\to y\in \left\{x\right\}$$
8		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
9		equcomi	$$⊢y=x\to x=y$$
10	8 9	sylbi	$$⊢y\in \left\{x\right\}\to x=y$$
11	7 10	syl	$$⊢\forall z\left(x\in z\to y\in z\right)\to x=y$$