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

Theorem riotacl2 6524
 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 2903 . . 3 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 iotacl 5791 . . 3 (∃!𝑥(𝑥𝐴𝜑) → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
31, 2sylbi 206 . 2 (∃!𝑥𝐴 𝜑 → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
4 df-riota 6511 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
5 df-rab 2905 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
63, 4, 53eltr4g 2705 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃!weu 2458  {cab 2596  ∃!wreu 2898  {crab 2900  ℩cio 5766  ℩crio 6510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-un 3545  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-riota 6511 This theorem is referenced by:  riotacl  6525  riotasbc  6526  riotaxfrd  6541  supub  8248  suplub  8249  ordtypelem3  8308  catlid  16167  catrid  16168  grplinv  17291  pj1id  17935  evlsval2  19341  ig1pval3  23738  coelem  23786  quotlem  23859  mircgr  25352  mirbtwn  25353  grpoidinv2  26753  grpoinv  26763  cnlnadjlem5  28314  cvmsiota  30513  cvmliftiota  30537  mpaalem  36741  disjinfi  38375
 Copyright terms: Public domain W3C validator