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

Theorem riotabidv 6279
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 715 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5586 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
4 df-riota 6277 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
5 df-riota 6277 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
63, 4, 53eqtr4g 2521 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455    e. wcel 1898   iotacio 5563   iota_crio 6276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-uni 4213  df-iota 5565  df-riota 6277
This theorem is referenced by:  riotaeqbidv  6280  csbriota  6289  sup0riota  8005  infval  8028  fin23lem27  8784  subval  9892  divval  10300  flval  12062  ceilval2  12101  cjval  13214  sqrtval  13349  qnumval  14735  qdenval  14736  lubval  16279  glbval  16292  joinval2  16304  meetval2  16318  grpinvval  16754  pj1fval  17393  pj1val  17394  q1pval  23153  coeval  23226  quotval  23294  ismidb  24869  lmif  24876  islmib  24878  usgraidx2v  25169  nbgraf1olem4  25221  frgrancvvdeqlemB  25815  frgrancvvdeqlemC  25816  grpoinvval  26002  pjhval  27099  nmopadjlei  27790  cdj3lem2  28137  cvmliftlem15  30070  cvmlift2lem4  30078  cvmlift2  30088  cvmlift3lem2  30092  cvmlift3lem4  30094  cvmlift3lem6  30096  cvmlift3lem7  30097  cvmlift3lem9  30099  cvmlift3  30100  fvtransport  30848  lshpkrlem1  32721  lshpkrlem2  32722  lshpkrlem3  32723  lshpkrcl  32727  trlset  33772  trlval  33773  cdleme27b  33980  cdleme29b  33987  cdleme31so  33991  cdleme31sn1  33993  cdleme31sn1c  34000  cdleme31fv  34002  cdlemefrs29clN  34011  cdleme40v  34081  cdlemg1cN  34199  cdlemg1cex  34200  cdlemksv  34456  cdlemkuu  34507  cdlemkid3N  34545  cdlemkid4  34546  cdlemm10N  34731  dicval  34789  dihval  34845  dochfl1  35089  lcfl7N  35114  lcfrlem8  35162  lcfrlem9  35163  lcf1o  35164  mapdhval  35337  hvmapval  35373  hvmapvalvalN  35374  hdmap1fval  35410  hdmap1vallem  35411  hdmap1val  35412  hdmap1cbv  35416  hdmapfval  35443  hdmapval  35444  hgmapffval  35501  hgmapfval  35502  hgmapval  35503  unxpwdom3  35998  mpaaval  36062  uspgredg2v  39351  usgredg2v  39354  usgedgvadf1  40000  usgedgvadf1ALT  40003
  Copyright terms: Public domain W3C validator