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

Theorem riotabidv 6247
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 biidd 237 . . . 4  |-  ( ph  ->  ( x  e.  A  <->  x  e.  A ) )
2 riotabidv.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2anbi12d 710 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5572 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 df-riota 6245 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
6 df-riota 6245 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
74, 5, 63eqtr4g 2533 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   iotacio 5549   iota_crio 6244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-iota 5551  df-riota 6245
This theorem is referenced by:  riotaeqbidv  6248  csbriota  6257  fin23lem27  8708  subval  9811  divval  10209  flval  11899  ceilval2  11937  cjval  12898  sqrtval  13033  qnumval  14129  qdenval  14130  lubval  15471  glbval  15484  joinval2  15496  meetval2  15510  grpinvval  15899  pj1fval  16518  pj1val  16519  q1pval  22317  coeval  22383  quotval  22450  ismidb  23849  lmif  23856  islmib  23858  usgraidx2v  24097  nbgraf1olem4  24148  frgrancvvdeqlemB  24743  frgrancvvdeqlemC  24744  grpoinvval  24931  pjhval  26019  nmopadjlei  26711  cdj3lem2  27058  cvmliftlem15  28411  cvmlift2lem4  28419  cvmlift2  28429  cvmlift3lem2  28433  cvmlift3lem4  28435  cvmlift3lem6  28437  cvmlift3lem7  28438  cvmlift3lem9  28440  cvmlift3  28441  fvtransport  29287  unxpwdom3  30673  mpaaval  30733  usgedgvadf1  31910  usgedgvadf1ALT  31913  lshpkrlem1  33925  lshpkrlem2  33926  lshpkrlem3  33927  lshpkrcl  33931  trlset  34975  trlval  34976  cdleme27b  35182  cdleme29b  35189  cdleme31so  35193  cdleme31sn1  35195  cdleme31sn1c  35202  cdleme31fv  35204  cdlemefrs29clN  35213  cdleme40v  35283  cdlemg1cN  35401  cdlemg1cex  35402  cdlemksv  35658  cdlemkuu  35709  cdlemkid3N  35747  cdlemkid4  35748  cdlemm10N  35933  dicval  35991  dihval  36047  dochfl1  36291  lcfl7N  36316  lcfrlem8  36364  lcfrlem9  36365  lcf1o  36366  mapdhval  36539  hvmapval  36575  hvmapvalvalN  36576  hdmap1fval  36612  hdmap1vallem  36613  hdmap1val  36614  hdmap1cbv  36618  hdmapfval  36645  hdmapval  36646  hgmapffval  36703  hgmapfval  36704  hgmapval  36705
  Copyright terms: Public domain W3C validator