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

Theorem riotabidv 6268
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 )
)
21anbi2d 709 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5585 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
4 df-riota 6266 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
5 df-riota 6266 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
63, 4, 53eqtr4g 2489 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438    e. wcel 1869   iotacio 5562   iota_crio 6265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-uni 4219  df-iota 5564  df-riota 6266
This theorem is referenced by:  riotaeqbidv  6269  csbriota  6278  sup0riota  7987  infval  8010  fin23lem27  8764  subval  9872  divval  10278  flval  12035  ceilval2  12074  cjval  13163  sqrtval  13298  qnumval  14683  qdenval  14684  lubval  16227  glbval  16240  joinval2  16252  meetval2  16266  grpinvval  16702  pj1fval  17341  pj1val  17342  q1pval  23100  coeval  23173  quotval  23241  ismidb  24816  lmif  24823  islmib  24825  usgraidx2v  25116  nbgraf1olem4  25168  frgrancvvdeqlemB  25762  frgrancvvdeqlemC  25763  grpoinvval  25949  pjhval  27046  nmopadjlei  27737  cdj3lem2  28084  cvmliftlem15  30027  cvmlift2lem4  30035  cvmlift2  30045  cvmlift3lem2  30049  cvmlift3lem4  30051  cvmlift3lem6  30053  cvmlift3lem7  30054  cvmlift3lem9  30056  cvmlift3  30057  fvtransport  30802  lshpkrlem1  32643  lshpkrlem2  32644  lshpkrlem3  32645  lshpkrcl  32649  trlset  33694  trlval  33695  cdleme27b  33902  cdleme29b  33909  cdleme31so  33913  cdleme31sn1  33915  cdleme31sn1c  33922  cdleme31fv  33924  cdlemefrs29clN  33933  cdleme40v  34003  cdlemg1cN  34121  cdlemg1cex  34122  cdlemksv  34378  cdlemkuu  34429  cdlemkid3N  34467  cdlemkid4  34468  cdlemm10N  34653  dicval  34711  dihval  34767  dochfl1  35011  lcfl7N  35036  lcfrlem8  35084  lcfrlem9  35085  lcf1o  35086  mapdhval  35259  hvmapval  35295  hvmapvalvalN  35296  hdmap1fval  35332  hdmap1vallem  35333  hdmap1val  35334  hdmap1cbv  35338  hdmapfval  35365  hdmapval  35366  hgmapffval  35423  hgmapfval  35424  hgmapval  35425  unxpwdom3  35921  mpaaval  35985  usgridx2v  38975  usgedgvadf1  39119  usgedgvadf1ALT  39122
  Copyright terms: Public domain W3C validator