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

Theorem riotabidv 6308
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 2726 . . 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 5242 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2286 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3589 . 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 6306 . 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 6306 . 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 2342 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 1625    e. wcel 1686   {cab 2271   E!wreu 2547   ifcif 3567   iotacio 5219   ` cfv 5257   Undefcund 6298   iota_crio 6299
This theorem is referenced by:  riotaeqbidv  6309  csbriotag  6319  fin23lem27  7956  subval  9045  divval  9428  flval  10928  cjval  11589  sqrval  11724  qnumval  12810  qdenval  12811  lubval  14115  glbval  14120  joinval2  14125  meetval2  14132  spwval2  14335  spwpr4  14342  grpinvval  14523  pj1fval  15005  pj1val  15006  q1pval  19541  coeval  19607  quotval  19674  grpoinvval  20894  pjhval  21978  nmopadjlei  22670  cdj3lem2  23017  cvmliftlem15  23831  cvmlift2lem4  23839  cvmlift2  23849  cvmlift3lem2  23853  cvmlift3lem4  23855  cvmlift3lem6  23857  cvmlift3lem7  23858  cvmlift3lem9  23860  cvmlift3  23861  fvtransport  24657  issubcv  25681  lineval222  26090  lineval3a  26094  lineval4a  26098  unxpwdom3  27267  mpaaval  27367  frgra2v  28188  lshpkrlem1  29373  lshpkrlem2  29374  lshpkrlem3  29375  lshpkrcl  29379  trlset  30423  trlval  30424  cdleme27b  30630  cdleme29b  30637  cdleme31so  30641  cdleme31sn1  30643  cdleme31sn1c  30650  cdleme31fv  30652  cdlemefrs29clN  30661  cdleme40v  30731  cdlemg1cN  30849  cdlemg1cex  30850  cdlemksv  31106  cdlemkuu  31157  cdlemkid3N  31195  cdlemkid4  31196  cdlemm10N  31381  dicval  31439  dihval  31495  dochfl1  31739  lcfl7N  31764  lcfrlem8  31812  lcfrlem9  31813  lcf1o  31814  mapdhval  31987  hvmapval  32023  hvmapvalvalN  32024  hdmap1fval  32060  hdmap1vallem  32061  hdmap1val  32062  hdmap1cbv  32066  hdmapfval  32093  hdmapval  32094  hgmapffval  32151  hgmapfval  32152  hgmapval  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-un 3159  df-if 3568  df-uni 3830  df-iota 5221  df-riota 6306
  Copyright terms: Public domain W3C validator