Theorem abbi1sn

Description: Originally part of uniabio . Convert a theorem about df-iota to one about dfiota2 , without ax-10 , ax-11 , ax-12 . Although, eu6 uses ax-10 and ax-12 . (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Assertion	abbi1sn	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } )
2		df-sn	⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
3	1 2	eqtr4di	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )