Theorem absn 4609

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

Assertion

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

Distinct variable group:   𝑥,𝑌

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem absn

Step	Hyp	Ref	Expression
1		df-sn 4590	. . 3 ⊢ {𝑌} = {𝑥 ∣ 𝑥 = 𝑌}
2	1	eqeq2i 2776	. 2 ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝑥 = 𝑌})
3		abbib 2832	. 2 ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝑥 = 𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
4	2, 3	bitri 278	1 ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568   = wceq 1570  {cab 2741  {csn 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-sn 4590

This theorem is used by:  rabeqsn  4633  euabsn2  4691  dfiota2  6493  n0cut  28536  dfaiota2  47851  aiotaval  47860