Theorem absn

Description: Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 . (Contributed by Andrew Salmon, 30-Jun-2011) (Revised by AV, 24-Aug-2022)

	Ref	Expression
Assertion	absn	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sn	⊢ { 𝑌 } = { 𝑥 ∣ 𝑥 = 𝑌 }
2	1	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } )
3		abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } )
4	2 3	bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )