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

Theorem riotacl2 7124
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 3150 . . 3 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 iotacl 6340 . . 3 (∃!𝑥(𝑥𝐴𝜑) → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
31, 2sylbi 218 . 2 (∃!𝑥𝐴 𝜑 → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
4 df-riota 7108 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
5 df-rab 3152 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
63, 4, 53eltr4g 2935 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  ∃!weu 2651  {cab 2804  ∃!wreu 3145  {crab 3147  cio 6311  crio 7107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-un 3945  df-sn 4565  df-pr 4567  df-uni 4838  df-iota 6313  df-riota 7108
This theorem is referenced by:  riotacl  7125  riotasbc  7126  riotaxfrd  7142  supub  8917  suplub  8918  ordtypelem3  8978  catlid  16949  catrid  16950  grplinv  18097  pj1id  18761  evlsval2  20235  ig1pval3  24702  coelem  24750  quotlem  24823  mircgr  26376  mirbtwn  26377  grpoidinv2  28225  grpoinv  28235  cnlnadjlem5  29781  cvmsiota  32427  cvmliftiota  32451  mpaalem  39636  disjinfi  41338
  Copyright terms: Public domain W3C validator