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

Theorem riotacl2 6767
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 3068 . . 3 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 iotacl 6017 . . 3 (∃!𝑥(𝑥𝐴𝜑) → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
31, 2sylbi 207 . 2 (∃!𝑥𝐴 𝜑 → (℩𝑥(𝑥𝐴𝜑)) ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
4 df-riota 6754 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
5 df-rab 3070 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
63, 4, 53eltr4g 2867 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  ∃!weu 2618  {cab 2757  ∃!wreu 3063  {crab 3065  cio 5992  crio 6753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-un 3728  df-sn 4317  df-pr 4319  df-uni 4575  df-iota 5994  df-riota 6754
This theorem is referenced by:  riotacl  6768  riotasbc  6769  riotaxfrd  6785  supub  8521  suplub  8522  ordtypelem3  8581  catlid  16551  catrid  16552  grplinv  17676  pj1id  18319  evlsval2  19735  ig1pval3  24154  coelem  24202  quotlem  24275  mircgr  25773  mirbtwn  25774  grpoidinv2  27709  grpoinv  27719  cnlnadjlem5  29270  cvmsiota  31597  cvmliftiota  31621  mpaalem  38248  disjinfi  39900
  Copyright terms: Public domain W3C validator