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

Theorem riotabidv 6054
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 5402 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 df-riota 6052 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
6 df-riota 6052 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
74, 5, 63eqtr4g 2500 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 1369    e. wcel 1756   iotacio 5379   iota_crio 6051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-uni 4092  df-iota 5381  df-riota 6052
This theorem is referenced by:  riotaeqbidv  6055  csbriota  6064  fin23lem27  8497  subval  9601  divval  9996  flval  11644  ceilval2  11681  cjval  12591  sqrval  12726  qnumval  13815  qdenval  13816  lubval  15154  glbval  15167  joinval2  15179  meetval2  15193  grpinvval  15577  pj1fval  16191  pj1val  16192  q1pval  21625  coeval  21691  quotval  21758  usgraidx2v  23311  nbgraf1olem4  23353  grpoinvval  23712  pjhval  24800  nmopadjlei  25492  cdj3lem2  25839  cvmliftlem15  27187  cvmlift2lem4  27195  cvmlift2  27205  cvmlift3lem2  27209  cvmlift3lem4  27211  cvmlift3lem6  27213  cvmlift3lem7  27214  cvmlift3lem9  27216  cvmlift3  27217  fvtransport  28063  unxpwdom3  29448  mpaaval  29508  frgrancvvdeqlemB  30631  frgrancvvdeqlemC  30632  lshpkrlem1  32755  lshpkrlem2  32756  lshpkrlem3  32757  lshpkrcl  32761  trlset  33805  trlval  33806  cdleme27b  34012  cdleme29b  34019  cdleme31so  34023  cdleme31sn1  34025  cdleme31sn1c  34032  cdleme31fv  34034  cdlemefrs29clN  34043  cdleme40v  34113  cdlemg1cN  34231  cdlemg1cex  34232  cdlemksv  34488  cdlemkuu  34539  cdlemkid3N  34577  cdlemkid4  34578  cdlemm10N  34763  dicval  34821  dihval  34877  dochfl1  35121  lcfl7N  35146  lcfrlem8  35194  lcfrlem9  35195  lcf1o  35196  mapdhval  35369  hvmapval  35405  hvmapvalvalN  35406  hdmap1fval  35442  hdmap1vallem  35443  hdmap1val  35444  hdmap1cbv  35448  hdmapfval  35475  hdmapval  35476  hgmapffval  35533  hgmapfval  35534  hgmapval  35535
  Copyright terms: Public domain W3C validator