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

Theorem riotabidv 6487
Description: Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.)
Hypothesis
Ref Expression
riotabidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
riotabidv  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem riotabidv
StepHypRef Expression
1 riotabidv.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21reubidv 2835 . . 3  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
31anbi2d 685 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5379 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2388 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3704 . 2  |-  ( ph  ->  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )  =  if ( E! x  e.  A  ch ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) ) )
7 df-riota 6485 . 2  |-  ( iota_ x  e.  A ps )  =  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
8 df-riota 6485 . 2  |-  ( iota_ x  e.  A ch )  =  if ( E! x  e.  A  ch ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
96, 7, 83eqtr4g 2444 1  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   {cab 2373   E!wreu 2651   ifcif 3682   iotacio 5356   ` cfv 5394   Undefcund 6477   iota_crio 6478
This theorem is referenced by:  riotaeqbidv  6488  csbriotag  6498  fin23lem27  8141  subval  9229  divval  9612  flval  11130  cjval  11834  sqrval  11969  qnumval  13056  qdenval  13057  lubval  14363  glbval  14368  joinval2  14373  meetval2  14380  spwval2  14583  spwpr4  14590  grpinvval  14771  pj1fval  15253  pj1val  15254  q1pval  19943  coeval  20009  quotval  20076  usgraidx2v  21278  nbgraf1olem4  21320  grpoinvval  21661  pjhval  22747  nmopadjlei  23439  cdj3lem2  23786  cvmliftlem15  24764  cvmlift2lem4  24772  cvmlift2  24782  cvmlift3lem2  24786  cvmlift3lem4  24788  cvmlift3lem6  24790  cvmlift3lem7  24791  cvmlift3lem9  24793  cvmlift3  24794  fvtransport  25680  unxpwdom3  26925  mpaaval  27025  frgra2v  27752  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  lshpkrlem1  29225  lshpkrlem2  29226  lshpkrlem3  29227  lshpkrcl  29231  trlset  30275  trlval  30276  cdleme27b  30482  cdleme29b  30489  cdleme31so  30493  cdleme31sn1  30495  cdleme31sn1c  30502  cdleme31fv  30504  cdlemefrs29clN  30513  cdleme40v  30583  cdlemg1cN  30701  cdlemg1cex  30702  cdlemksv  30958  cdlemkuu  31009  cdlemkid3N  31047  cdlemkid4  31048  cdlemm10N  31233  dicval  31291  dihval  31347  dochfl1  31591  lcfl7N  31616  lcfrlem8  31664  lcfrlem9  31665  lcf1o  31666  mapdhval  31839  hvmapval  31875  hvmapvalvalN  31876  hdmap1fval  31912  hdmap1vallem  31913  hdmap1val  31914  hdmap1cbv  31918  hdmapfval  31945  hdmapval  31946  hgmapffval  32003  hgmapfval  32004  hgmapval  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-un 3268  df-if 3683  df-uni 3958  df-iota 5358  df-riota 6485
  Copyright terms: Public domain W3C validator