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

Theorem riotacl2 6151
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 2799 . . 3  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
2 iotacl 5488 . . 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 6137 . 2  |-  ( iota_ x  e.  A  ph )  =  ( iota x
( x  e.  A  /\  ph ) )
5 df-rab 2801 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
63, 4, 53eltr4g 2554 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 369    e. wcel 1757   E!weu 2259   {cab 2435   E!wreu 2794   {crab 2796   iotacio 5463   iota_crio 6136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3056  df-sbc 3271  df-un 3417  df-sn 3962  df-pr 3964  df-uni 4176  df-iota 5465  df-riota 6137
This theorem is referenced by:  riotacl  6152  riotasbc  6153  riotaxfrd  6168  supub  7796  suplub  7797  ordtypelem3  7821  catlid  14709  catrid  14710  grplinv  15672  pj1id  16286  evlsval2  17699  ig1pval3  21748  coelem  21796  quotlem  21868  mircgr  23173  mirbtwn  23174  grpoidinv2  23826  grpoinv  23835  cnlnadjlem5  25596  cvmsiota  27286  cvmliftiota  27310  mpaalem  29633
  Copyright terms: Public domain W3C validator