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

Theorem riotabidv 6543
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 2884 . . 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 5431 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2436 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3753 . 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 6541 . 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 6541 . 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 2492 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 1652    e. wcel 1725   {cab 2421   E!wreu 2699   ifcif 3731   iotacio 5408   ` cfv 5446   Undefcund 6533   iota_crio 6534
This theorem is referenced by:  riotaeqbidv  6544  csbriotag  6554  fin23lem27  8200  subval  9289  divval  9672  flval  11195  cjval  11899  sqrval  12034  qnumval  13121  qdenval  13122  lubval  14428  glbval  14433  joinval2  14438  meetval2  14445  spwval2  14648  spwpr4  14655  grpinvval  14836  pj1fval  15318  pj1val  15319  q1pval  20068  coeval  20134  quotval  20201  usgraidx2v  21404  nbgraf1olem4  21446  grpoinvval  21805  pjhval  22891  nmopadjlei  23583  cdj3lem2  23930  cvmliftlem15  24977  cvmlift2lem4  24985  cvmlift2  24995  cvmlift3lem2  24999  cvmlift3lem4  25001  cvmlift3lem6  25003  cvmlift3lem7  25004  cvmlift3lem9  25006  cvmlift3  25007  fvtransport  25958  unxpwdom3  27224  mpaaval  27324  frgra2v  28326  frgrancvvdeqlemB  28364  frgrancvvdeqlemC  28365  lshpkrlem1  29845  lshpkrlem2  29846  lshpkrlem3  29847  lshpkrcl  29851  trlset  30895  trlval  30896  cdleme27b  31102  cdleme29b  31109  cdleme31so  31113  cdleme31sn1  31115  cdleme31sn1c  31122  cdleme31fv  31124  cdlemefrs29clN  31133  cdleme40v  31203  cdlemg1cN  31321  cdlemg1cex  31322  cdlemksv  31578  cdlemkuu  31629  cdlemkid3N  31667  cdlemkid4  31668  cdlemm10N  31853  dicval  31911  dihval  31967  dochfl1  32211  lcfl7N  32236  lcfrlem8  32284  lcfrlem9  32285  lcf1o  32286  mapdhval  32459  hvmapval  32495  hvmapvalvalN  32496  hdmap1fval  32532  hdmap1vallem  32533  hdmap1val  32534  hdmap1cbv  32538  hdmapfval  32565  hdmapval  32566  hgmapffval  32623  hgmapfval  32624  hgmapval  32625
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-un 3317  df-if 3732  df-uni 4008  df-iota 5410  df-riota 6541
  Copyright terms: Public domain W3C validator