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

Theorem riotabidv 6244
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 703 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5562 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
4 df-riota 6242 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
5 df-riota 6242 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
63, 4, 53eqtr4g 2509 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 1383    e. wcel 1804   iotacio 5539   iota_crio 6241
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235  df-iota 5541  df-riota 6242
This theorem is referenced by:  riotaeqbidv  6245  csbriota  6254  fin23lem27  8711  subval  9816  divval  10216  flval  11913  ceilval2  11951  cjval  12917  sqrtval  13052  qnumval  14252  qdenval  14253  lubval  15593  glbval  15606  joinval2  15618  meetval2  15632  grpinvval  16068  pj1fval  16691  pj1val  16692  q1pval  22532  coeval  22598  quotval  22666  ismidb  24122  lmif  24129  islmib  24131  usgraidx2v  24371  nbgraf1olem4  24422  frgrancvvdeqlemB  25016  frgrancvvdeqlemC  25017  grpoinvval  25205  pjhval  26293  nmopadjlei  26985  cdj3lem2  27332  cvmliftlem15  28721  cvmlift2lem4  28729  cvmlift2  28739  cvmlift3lem2  28743  cvmlift3lem4  28745  cvmlift3lem6  28747  cvmlift3lem7  28748  cvmlift3lem9  28750  cvmlift3  28751  fvtransport  29658  unxpwdom3  31017  mpaaval  31076  usgedgvadf1  32369  usgedgvadf1ALT  32372  lshpkrlem1  34710  lshpkrlem2  34711  lshpkrlem3  34712  lshpkrcl  34716  trlset  35761  trlval  35762  cdleme27b  35969  cdleme29b  35976  cdleme31so  35980  cdleme31sn1  35982  cdleme31sn1c  35989  cdleme31fv  35991  cdlemefrs29clN  36000  cdleme40v  36070  cdlemg1cN  36188  cdlemg1cex  36189  cdlemksv  36445  cdlemkuu  36496  cdlemkid3N  36534  cdlemkid4  36535  cdlemm10N  36720  dicval  36778  dihval  36834  dochfl1  37078  lcfl7N  37103  lcfrlem8  37151  lcfrlem9  37152  lcf1o  37153  mapdhval  37326  hvmapval  37362  hvmapvalvalN  37363  hdmap1fval  37399  hdmap1vallem  37400  hdmap1val  37401  hdmap1cbv  37405  hdmapfval  37432  hdmapval  37433  hgmapffval  37490  hgmapfval  37491  hgmapval  37492
  Copyright terms: Public domain W3C validator