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

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

This can useful for expanding an iota-based definition (see df-iota 5219). If you have an unbounded iota, iotacl 5242 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 6310 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  =  ( iota x ( x  e.  A  /\  ph )
) )
2 df-reu 2550 . . . 4  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 iotacl 5242 . . . 4  |-  ( E! x ( x  e.  A  /\  ph )  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
42, 3sylbi 187 . . 3  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
5 df-rab 2552 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
64, 5syl6eleqr 2374 . 2  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  e.  A  |  ph } )
71, 6eqeltrd 2357 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 358    e. wcel 1684   E!weu 2143   {cab 2269   E!wreu 2545   {crab 2547   iotacio 5217   iota_crio 6297
This theorem is referenced by:  riotacl  6319  riotasbc  6320  riotaxfrd  6336  supub  7210  suplub  7211  ordtypelem3  7235  catlid  13585  catrid  13586  grplinv  14528  pj1id  15008  evlsval2  19404  ig1pval3  19560  coelem  19608  quotlem  19680  grpoidinv2  20885  grpoinv  20894  cnlnadjlem5  22651  cvmsiota  23808  cvmliftiota  23832  supdef  25262  mpaalem  27357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-un 3157  df-if 3566  df-sn 3646  df-pr 3647  df-uni 3828  df-iota 5219  df-riota 6304
  Copyright terms: Public domain W3C validator