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

Theorem riotaeqbidv 6241
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
Hypotheses
Ref Expression
riotaeqbidv.1  |-  ( ph  ->  A  =  B )
riotaeqbidv.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
riotaeqbidv  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  B  ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)    B( x)

Proof of Theorem riotaeqbidv
StepHypRef Expression
1 riotaeqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21riotabidv 6240 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
3 riotaeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
43riotaeqdv 6239 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ch )  =  ( iota_ x  e.  B  ch ) )
52, 4eqtrd 2482 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  B  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381   iota_crio 6237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-uni 4231  df-iota 5537  df-riota 6238
This theorem is referenced by:  dfoi  7934  oieq1  7935  oieq2  7936  ordtypecbv  7940  ordtypelem3  7943  zorn2lem1  8874  zorn2g  8881  cidfval  14945  cidval  14946  cidpropd  14977  lubfval  15477  glbfval  15490  grpinvfval  15957  pj1fval  16581  mpfrcl  18055  evlsval  18056  q1pval  22420  ig1pval  22439  mirval  23901  midf  24007  ismidb  24009  lmif  24016  islmib  24018  gidval  25080  grpoinvfval  25091  pjhfval  26179  cvmliftlem5  28600  cvmliftlem15  28609  trlfset  35587  dicffval  36603  dicfval  36604  dihffval  36659  dihfval  36660  hvmapffval  37187  hvmapfval  37188  hdmap1fval  37226  hdmapffval  37258  hdmapfval  37259  hgmapfval  37318
  Copyright terms: Public domain W3C validator