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

Theorem riotacl2 6193
Description: Membership law for "the unique element in  A such that  ph."

(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Assertion
Ref Expression
riotacl2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)

Proof of Theorem riotacl2
StepHypRef Expression
1 df-reu 2753 . . 3  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
2 iotacl 5500 . . 3  |-  ( E! x ( x  e.  A  /\  ph )  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
31, 2sylbi 195 . 2  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
4 df-riota 6180 . 2  |-  ( iota_ x  e.  A  ph )  =  ( iota x
( x  e.  A  /\  ph ) )
5 df-rab 2755 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
63, 4, 53eltr4g 2502 1  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1836   E!weu 2232   {cab 2381   E!wreu 2748   {crab 2750   iotacio 5475   iota_crio 6179
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-un 3411  df-sn 3962  df-pr 3964  df-uni 4181  df-iota 5477  df-riota 6180
This theorem is referenced by:  riotacl  6194  riotasbc  6195  riotaxfrd  6210  supub  7855  suplub  7856  ordtypelem3  7882  catlid  15113  catrid  15114  grplinv  16236  pj1id  16857  evlsval2  18325  ig1pval3  22683  coelem  22731  quotlem  22804  mircgr  24183  mirbtwn  24184  grpoidinv2  25362  grpoinv  25371  cnlnadjlem5  27131  cvmsiota  28951  cvmliftiota  28975  mpaalem  31309
  Copyright terms: Public domain W3C validator