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

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

This can useful for expanding an iota-based definition (see df-iota 5447). If you have an unbounded iota, iotacl 5470 may be useful.

(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 riotaiota 6584 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  =  ( iota x ( x  e.  A  /\  ph )
) )
2 df-reu 2718 . . . 4  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 iotacl 5470 . . . 4  |-  ( E! x ( x  e.  A  /\  ph )  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
42, 3sylbi 189 . . 3  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
5 df-rab 2720 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
64, 5syl6eleqr 2533 . 2  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  e.  A  |  ph } )
71, 6eqeltrd 2516 1  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  e.  { x  e.  A  |  ph }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1727   E!weu 2287   {cab 2428   E!wreu 2713   {crab 2715   iotacio 5445   iota_crio 6571
This theorem is referenced by:  riotacl  6593  riotasbc  6594  riotaxfrd  6610  supub  7493  suplub  7494  ordtypelem3  7518  catlid  13939  catrid  13940  grplinv  14882  pj1id  15362  evlsval2  19972  ig1pval3  20128  coelem  20176  quotlem  20248  grpoidinv2  21837  grpoinv  21846  cnlnadjlem5  23605  cvmsiota  24995  cvmliftiota  25019  mpaalem  27372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-un 3311  df-if 3764  df-sn 3844  df-pr 3845  df-uni 4040  df-iota 5447  df-riota 6578
  Copyright terms: Public domain W3C validator