MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riotacl2 Structured version   Visualization version   GIF version

Theorem riotacl2 6815
Description: Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
Assertion
Ref Expression
riotacl2 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})

Proof of Theorem riotacl2
StepHypRef Expression
1 df-reu 3061 . . 3 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 iotacl 6053 . . 3 (∃!𝑥(𝑥𝐴𝜑) → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
31, 2sylbi 208 . 2 (∃!𝑥𝐴 𝜑 → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
4 df-riota 6802 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
5 df-rab 3063 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
63, 4, 53eltr4g 2860 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155  ∃!weu 2580  {cab 2750  ∃!wreu 3056  {crab 3058  cio 6028  crio 6801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-un 3736  df-sn 4334  df-pr 4336  df-uni 4594  df-iota 6030  df-riota 6802
This theorem is referenced by:  riotacl  6816  riotasbc  6817  riotaxfrd  6833  supub  8571  suplub  8572  ordtypelem3  8631  catlid  16610  catrid  16611  grplinv  17736  pj1id  18377  evlsval2  19792  ig1pval3  24224  coelem  24272  quotlem  24345  mircgr  25842  mirbtwn  25843  grpoidinv2  27760  grpoinv  27770  cnlnadjlem5  29320  cvmsiota  31638  cvmliftiota  31662  mpaalem  38331  disjinfi  39959
  Copyright terms: Public domain W3C validator