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	⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		vsnid	⊢ 𝑥 ∈ { 𝑥 }
2		vsnex	⊢ { 𝑥 } ∈ V
3		eleq2	⊢ ( 𝑧 = { 𝑥 } → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ { 𝑥 } ) )
4		eleq2	⊢ ( 𝑧 = { 𝑥 } → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑥 } ) )
5	3 4	imbi12d	⊢ ( 𝑧 = { 𝑥 } → ( ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ↔ ( 𝑥 ∈ { 𝑥 } → 𝑦 ∈ { 𝑥 } ) ) )
6	2 5	spcv	⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ { 𝑥 } → 𝑦 ∈ { 𝑥 } ) )
7	1 6	mpi	⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑦 ∈ { 𝑥 } )
8		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
9		equcomi	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
10	8 9	sylbi	⊢ ( 𝑦 ∈ { 𝑥 } → 𝑥 = 𝑦 )
11	7 10	syl	⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 )