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

Theorem riotacl2 7385
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 3376 . . 3 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 iotacl 6529 . . 3 (∃!𝑥(𝑥𝐴𝜑) → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
31, 2sylbi 216 . 2 (∃!𝑥𝐴 𝜑 → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
4 df-riota 7368 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
5 df-rab 3432 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
63, 4, 53eltr4g 2849 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2105  ∃!weu 2561  {cab 2708  ∃!wreu 3373  {crab 3431  cio 6493  crio 7367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6495  df-riota 7368
This theorem is referenced by:  riotacl  7386  riotasbc  7387  riotaxfrd  7403  supub  9457  suplub  9458  ordtypelem3  9518  catlid  17632  catrid  17633  grplinv  18911  pj1id  19609  evlsval2  21870  ig1pval3  25928  coelem  25976  quotlem  26050  mircgr  28176  mirbtwn  28177  grpoidinv2  30036  grpoinv  30046  cnlnadjlem5  31592  cvmsiota  34567  cvmliftiota  34591  mpaalem  42197  disjinfi  44190
  Copyright terms: Public domain W3C validator