Theorem eusnsn

Description: There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	eusnsn	⊢ ∃! 𝑥 { 𝑥 } = { 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
2	1	bibi2d	⊢ ( 𝑧 = 𝑦 → ( ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑧 ) ↔ ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) ) )
3	2	albidv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) ) )
4		sneqbg	⊢ ( 𝑥 ∈ V → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) )
5	4	elv	⊢ ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 )
6	5	ax-gen	⊢ ∀ 𝑥 ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 )
7	3 6	speivw	⊢ ∃ 𝑧 ∀ 𝑥 ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑧 )
8		eu6	⊢ ( ∃! 𝑥 { 𝑥 } = { 𝑦 } ↔ ∃ 𝑧 ∀ 𝑥 ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑧 ) )
9	7 8	mpbir	⊢ ∃! 𝑥 { 𝑥 } = { 𝑦 }