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

Theorem riotabidv 6322
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 2737 . . 3  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
31anbi2d 684 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5256 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2297 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3600 . 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 6320 . 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 6320 . 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 2353 1  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {cab 2282   E!wreu 2558   ifcif 3578   iotacio 5233   ` cfv 5271   Undefcund 6312   iota_crio 6313
This theorem is referenced by:  riotaeqbidv  6323  csbriotag  6333  fin23lem27  7970  subval  9059  divval  9442  flval  10942  cjval  11603  sqrval  11738  qnumval  12824  qdenval  12825  lubval  14129  glbval  14134  joinval2  14139  meetval2  14146  spwval2  14349  spwpr4  14356  grpinvval  14537  pj1fval  15019  pj1val  15020  q1pval  19555  coeval  19621  quotval  19688  grpoinvval  20908  pjhval  21992  nmopadjlei  22684  cdj3lem2  23031  cvmliftlem15  23844  cvmlift2lem4  23852  cvmlift2  23862  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  cvmlift3  23874  fvtransport  24727  issubcv  25773  lineval222  26182  lineval3a  26186  lineval4a  26190  unxpwdom3  27359  mpaaval  27459  frgra2v  28423  lshpkrlem1  29922  lshpkrlem2  29923  lshpkrlem3  29924  lshpkrcl  29928  trlset  30972  trlval  30973  cdleme27b  31179  cdleme29b  31186  cdleme31so  31190  cdleme31sn1  31192  cdleme31sn1c  31199  cdleme31fv  31201  cdlemefrs29clN  31210  cdleme40v  31280  cdlemg1cN  31398  cdlemg1cex  31399  cdlemksv  31655  cdlemkuu  31706  cdlemkid3N  31744  cdlemkid4  31745  cdlemm10N  31930  dicval  31988  dihval  32044  dochfl1  32288  lcfl7N  32313  lcfrlem8  32361  lcfrlem9  32362  lcf1o  32363  mapdhval  32536  hvmapval  32572  hvmapvalvalN  32573  hdmap1fval  32609  hdmap1vallem  32610  hdmap1val  32611  hdmap1cbv  32615  hdmapfval  32642  hdmapval  32643  hgmapffval  32700  hgmapfval  32701  hgmapval  32702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-un 3170  df-if 3579  df-uni 3844  df-iota 5235  df-riota 6320
  Copyright terms: Public domain W3C validator