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

Theorem riotaeqbidv 6268
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 6267 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
3 riotaeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
43riotaeqdv 6266 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ch )  =  ( iota_ x  e.  B  ch ) )
52, 4eqtrd 2464 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  B  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   iota_crio 6264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-uni 4218  df-iota 5563  df-riota 6265
This theorem is referenced by:  dfoi  8030  oieq1  8031  oieq2  8032  ordtypecbv  8036  ordtypelem3  8039  zorn2lem1  8928  zorn2g  8935  cidfval  15575  cidval  15576  cidpropd  15608  lubfval  16217  glbfval  16230  grpinvfval  16697  pj1fval  17337  mpfrcl  18734  evlsval  18735  q1pval  23096  ig1pval  23116  ig1pvalOLD  23122  mirval  24692  midf  24810  ismidb  24812  lmif  24819  islmib  24821  gidval  25933  grpoinvfval  25944  pjhfval  27041  cvmliftlem5  30014  cvmliftlem15  30023  trlfset  33689  dicffval  34705  dicfval  34706  dihffval  34761  dihfval  34762  hvmapffval  35289  hvmapfval  35290  hdmap1fval  35328  hdmapffval  35360  hdmapfval  35361  hgmapfval  35420  wessf1ornlem  37353
  Copyright terms: Public domain W3C validator