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

Theorem riotabidv 6051
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 705 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5399 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 df-riota 6049 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
6 df-riota 6049 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
74, 5, 63eqtr4g 2498 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 1364    e. wcel 1761   iotacio 5376   iota_crio 6048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-uni 4089  df-iota 5378  df-riota 6049
This theorem is referenced by:  riotaeqbidv  6052  csbriota  6062  fin23lem27  8493  subval  9597  divval  9992  flval  11640  ceilval2  11677  cjval  12587  sqrval  12722  qnumval  13811  qdenval  13812  lubval  15150  glbval  15163  joinval2  15175  meetval2  15189  grpinvval  15570  pj1fval  16184  pj1val  16185  q1pval  21568  coeval  21634  quotval  21701  usgraidx2v  23230  nbgraf1olem4  23272  grpoinvval  23631  pjhval  24719  nmopadjlei  25411  cdj3lem2  25758  cvmliftlem15  27101  cvmlift2lem4  27109  cvmlift2  27119  cvmlift3lem2  27123  cvmlift3lem4  27125  cvmlift3lem6  27127  cvmlift3lem7  27128  cvmlift3lem9  27130  cvmlift3  27131  fvtransport  27976  unxpwdom3  29357  mpaaval  29417  frgrancvvdeqlemB  30540  frgrancvvdeqlemC  30541  lshpkrlem1  32443  lshpkrlem2  32444  lshpkrlem3  32445  lshpkrcl  32449  trlset  33493  trlval  33494  cdleme27b  33700  cdleme29b  33707  cdleme31so  33711  cdleme31sn1  33713  cdleme31sn1c  33720  cdleme31fv  33722  cdlemefrs29clN  33731  cdleme40v  33801  cdlemg1cN  33919  cdlemg1cex  33920  cdlemksv  34176  cdlemkuu  34227  cdlemkid3N  34265  cdlemkid4  34266  cdlemm10N  34451  dicval  34509  dihval  34565  dochfl1  34809  lcfl7N  34834  lcfrlem8  34882  lcfrlem9  34883  lcf1o  34884  mapdhval  35057  hvmapval  35093  hvmapvalvalN  35094  hdmap1fval  35130  hdmap1vallem  35131  hdmap1val  35132  hdmap1cbv  35136  hdmapfval  35163  hdmapval  35164  hgmapffval  35221  hgmapfval  35222  hgmapval  35223
  Copyright terms: Public domain W3C validator