This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Unordered and ordered pairs 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
abbib ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )
4
2 3
bitri ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )