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

Theorem riotaeqbidv 6307
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 6306 . 2  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
3 riotaeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
43riotaeqdv 6305 . 2  |-  ( ph  ->  ( iota_ x  e.  A ch )  =  ( iota_ x  e.  B ch ) )
52, 4eqtrd 2315 1  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  B ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   iota_crio 6297
This theorem is referenced by:  dfoi  7226  oieq1  7227  oieq2  7228  ordtypecbv  7232  ordtypelem3  7235  zorn2lem1  8123  zorn2g  8130  cidfval  13578  cidval  13579  cidpropd  13613  lubfval  14112  glbfval  14117  spwval2  14333  spwval  14334  grpinvfval  14520  pj1fval  15003  mpfrcl  19402  evlsval  19403  q1pval  19539  ig1pval  19558  gidval  20880  grpoinvfval  20891  pjhfval  21975  cvmliftlem5  23820  cvmliftlem15  23829  rngounval2  25425  issubcv  25670  trlfset  30349  dicffval  31364  dicfval  31365  dihffval  31420  dihfval  31421  hvmapffval  31948  hvmapfval  31949  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapfval  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-riota 6304
  Copyright terms: Public domain W3C validator