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

Theorem riotabidv 6160
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 701 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5481 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
4 df-riota 6158 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
5 df-riota 6158 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
63, 4, 53eqtr4g 2448 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 367    = wceq 1399    e. wcel 1826   iotacio 5458   iota_crio 6157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164  df-iota 5460  df-riota 6158
This theorem is referenced by:  riotaeqbidv  6161  csbriota  6170  fin23lem27  8621  subval  9724  divval  10126  flval  11830  ceilval2  11869  cjval  12937  sqrtval  13072  qnumval  14272  qdenval  14273  lubval  15731  glbval  15744  joinval2  15756  meetval2  15770  grpinvval  16206  pj1fval  16829  pj1val  16830  q1pval  22639  coeval  22705  quotval  22773  ismidb  24264  lmif  24271  islmib  24273  usgraidx2v  24514  nbgraf1olem4  24565  frgrancvvdeqlemB  25159  frgrancvvdeqlemC  25160  grpoinvval  25344  pjhval  26432  nmopadjlei  27123  cdj3lem2  27470  cvmliftlem15  28932  cvmlift2lem4  28940  cvmlift2  28950  cvmlift3lem2  28954  cvmlift3lem4  28956  cvmlift3lem6  28958  cvmlift3lem7  28959  cvmlift3lem9  28961  cvmlift3  28962  fvtransport  29835  unxpwdom3  31207  mpaaval  31268  usgedgvadf1  32733  usgedgvadf1ALT  32736  lshpkrlem1  35248  lshpkrlem2  35249  lshpkrlem3  35250  lshpkrcl  35254  trlset  36299  trlval  36300  cdleme27b  36507  cdleme29b  36514  cdleme31so  36518  cdleme31sn1  36520  cdleme31sn1c  36527  cdleme31fv  36529  cdlemefrs29clN  36538  cdleme40v  36608  cdlemg1cN  36726  cdlemg1cex  36727  cdlemksv  36983  cdlemkuu  37034  cdlemkid3N  37072  cdlemkid4  37073  cdlemm10N  37258  dicval  37316  dihval  37372  dochfl1  37616  lcfl7N  37641  lcfrlem8  37689  lcfrlem9  37690  lcf1o  37691  mapdhval  37864  hvmapval  37900  hvmapvalvalN  37901  hdmap1fval  37937  hdmap1vallem  37938  hdmap1val  37939  hdmap1cbv  37943  hdmapfval  37970  hdmapval  37971  hgmapffval  38028  hgmapfval  38029  hgmapval  38030
  Copyright terms: Public domain W3C validator