ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sniota GIF version

Theorem sniota 5226
Description: A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
Assertion
Ref Expression
sniota (∃!𝑥𝜑 → {𝑥𝜑} = {(℩𝑥𝜑)})

Proof of Theorem sniota
StepHypRef Expression
1 nfeu1 2049 . . 3 𝑥∃!𝑥𝜑
2 iota1 5210 . . . . 5 (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥))
3 eqcom 2191 . . . . 5 ((℩𝑥𝜑) = 𝑥𝑥 = (℩𝑥𝜑))
42, 3bitrdi 196 . . . 4 (∃!𝑥𝜑 → (𝜑𝑥 = (℩𝑥𝜑)))
5 abid 2177 . . . 4 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
6 vex 2755 . . . . 5 𝑥 ∈ V
76elsn 3623 . . . 4 (𝑥 ∈ {(℩𝑥𝜑)} ↔ 𝑥 = (℩𝑥𝜑))
84, 5, 73bitr4g 223 . . 3 (∃!𝑥𝜑 → (𝑥 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {(℩𝑥𝜑)}))
91, 8alrimi 1533 . 2 (∃!𝑥𝜑 → ∀𝑥(𝑥 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {(℩𝑥𝜑)}))
10 nfab1 2334 . . 3 𝑥{𝑥𝜑}
11 nfiota1 5198 . . . 4 𝑥(℩𝑥𝜑)
1211nfsn 3667 . . 3 𝑥{(℩𝑥𝜑)}
1310, 12cleqf 2357 . 2 ({𝑥𝜑} = {(℩𝑥𝜑)} ↔ ∀𝑥(𝑥 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {(℩𝑥𝜑)}))
149, 13sylibr 134 1 (∃!𝑥𝜑 → {𝑥𝜑} = {(℩𝑥𝜑)})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wal 1362   = wceq 1364  ∃!weu 2038  wcel 2160  {cab 2175  {csn 3607  cio 5194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-sn 3613  df-pr 3614  df-uni 3825  df-iota 5196
This theorem is referenced by:  snriota  5881
  Copyright terms: Public domain W3C validator