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

Theorem riotaeqbidv 6179
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 6178 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
3 riotaeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
43riotaeqdv 6177 . 2  |-  ( ph  ->  ( iota_ x  e.  A  ch )  =  ( iota_ x  e.  B  ch ) )
52, 4eqtrd 2433 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 1399   iota_crio 6175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rex 2748  df-uni 4177  df-iota 5473  df-riota 6176
This theorem is referenced by:  dfoi  7869  oieq1  7870  oieq2  7871  ordtypecbv  7875  ordtypelem3  7878  zorn2lem1  8807  zorn2g  8814  cidfval  15102  cidval  15103  cidpropd  15135  lubfval  15744  glbfval  15757  grpinvfval  16224  pj1fval  16848  mpfrcl  18319  evlsval  18320  q1pval  22658  ig1pval  22677  mirval  24177  midf  24283  ismidb  24285  lmif  24292  islmib  24294  gidval  25353  grpoinvfval  25364  pjhfval  26452  cvmliftlem5  28959  cvmliftlem15  28968  trlfset  36333  dicffval  37349  dicfval  37350  dihffval  37405  dihfval  37406  hvmapffval  37933  hvmapfval  37934  hdmap1fval  37972  hdmapffval  38004  hdmapfval  38005  hgmapfval  38064
  Copyright terms: Public domain W3C validator