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

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

This can useful for expanding an iota-based definition (see df-iota 5409). If you have an unbounded iota, iotacl 5432 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 6546 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  =  ( iota x ( x  e.  A  /\  ph )
) )
2 df-reu 2704 . . . 4  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 iotacl 5432 . . . 4  |-  ( E! x ( x  e.  A  /\  ph )  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
42, 3sylbi 188 . . 3  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  |  ( x  e.  A  /\  ph ) } )
5 df-rab 2706 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
64, 5syl6eleqr 2526 . 2  |-  ( E! x  e.  A  ph  ->  ( iota x ( x  e.  A  /\  ph ) )  e.  {
x  e.  A  |  ph } )
71, 6eqeltrd 2509 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 359    e. wcel 1725   E!weu 2280   {cab 2421   E!wreu 2699   {crab 2701   iotacio 5407   iota_crio 6533
This theorem is referenced by:  riotacl  6555  riotasbc  6556  riotaxfrd  6572  supub  7453  suplub  7454  ordtypelem3  7478  catlid  13896  catrid  13897  grplinv  14839  pj1id  15319  evlsval2  19929  ig1pval3  20085  coelem  20133  quotlem  20205  grpoidinv2  21794  grpoinv  21803  cnlnadjlem5  23562  cvmsiota  24952  cvmliftiota  24976  mpaalem  27272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-un 3317  df-if 3732  df-sn 3812  df-pr 3813  df-uni 4008  df-iota 5409  df-riota 6540
  Copyright terms: Public domain W3C validator