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

Theorem riotabidv 6306
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 2724 . . 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 5240 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2284 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3587 . 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 6304 . 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 6304 . 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 2340 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 1623    e. wcel 1684   {cab 2269   E!wreu 2545   ifcif 3565   iotacio 5217   ` cfv 5255   Undefcund 6296   iota_crio 6297
This theorem is referenced by:  riotaeqbidv  6307  csbriotag  6317  fin23lem27  7954  subval  9043  divval  9426  flval  10926  cjval  11587  sqrval  11722  qnumval  12808  qdenval  12809  lubval  14113  glbval  14118  joinval2  14123  meetval2  14130  spwval2  14333  spwpr4  14340  grpinvval  14521  pj1fval  15003  pj1val  15004  q1pval  19539  coeval  19605  quotval  19672  grpoinvval  20892  pjhval  21976  nmopadjlei  22668  cdj3lem2  23015  cvmliftlem15  23829  cvmlift2lem4  23837  cvmlift2  23847  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  fvtransport  24655  issubcv  25670  lineval222  26079  lineval3a  26083  lineval4a  26087  unxpwdom3  27256  mpaaval  27356  frgra2v  28177  lshpkrlem1  29300  lshpkrlem2  29301  lshpkrlem3  29302  lshpkrcl  29306  trlset  30350  trlval  30351  cdleme27b  30557  cdleme29b  30564  cdleme31so  30568  cdleme31sn1  30570  cdleme31sn1c  30577  cdleme31fv  30579  cdlemefrs29clN  30588  cdleme40v  30658  cdlemg1cN  30776  cdlemg1cex  30777  cdlemksv  31033  cdlemkuu  31084  cdlemkid3N  31122  cdlemkid4  31123  cdlemm10N  31308  dicval  31366  dihval  31422  dochfl1  31666  lcfl7N  31691  lcfrlem8  31739  lcfrlem9  31740  lcf1o  31741  mapdhval  31914  hvmapval  31950  hvmapvalvalN  31951  hdmap1fval  31987  hdmap1vallem  31988  hdmap1val  31989  hdmap1cbv  31993  hdmapfval  32020  hdmapval  32021  hgmapffval  32078  hgmapfval  32079  hgmapval  32080
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-un 3157  df-if 3566  df-uni 3828  df-iota 5219  df-riota 6304
  Copyright terms: Public domain W3C validator