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

Theorem riotaeqbidv 6076
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 6075 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
3 riotaeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
43riotaeqdv 6074 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ch )  =  ( iota_ x  e.  B  ch ) )
52, 4eqtrd 2475 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 1369   iota_crio 6072
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-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 2577  df-rex 2742  df-uni 4113  df-iota 5402  df-riota 6073
This theorem is referenced by:  dfoi  7746  oieq1  7747  oieq2  7748  ordtypecbv  7752  ordtypelem3  7755  zorn2lem1  8686  zorn2g  8693  cidfval  14635  cidval  14636  cidpropd  14670  lubfval  15169  glbfval  15182  grpinvfval  15597  pj1fval  16212  mpfrcl  17626  evlsval  17627  q1pval  21647  ig1pval  21666  mirval  23081  gidval  23722  grpoinvfval  23733  pjhfval  24821  cvmliftlem5  27200  cvmliftlem15  27209  trlfset  33900  dicffval  34915  dicfval  34916  dihffval  34971  dihfval  34972  hvmapffval  35499  hvmapfval  35500  hdmap1fval  35538  hdmapffval  35570  hdmapfval  35571  hgmapfval  35630
  Copyright terms: Public domain W3C validator