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

Theorem riotaeqbidv 7317
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
Hypotheses
Ref Expression
riotaeqbidv.1 (𝜑𝐴 = 𝐵)
riotaeqbidv.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
riotaeqbidv (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem riotaeqbidv
StepHypRef Expression
1 riotaeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
21riotabidv 7316 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 7315 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2777 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  crio 7313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-iota 6449  df-riota 7314
This theorem is referenced by:  dfoi  9448  oieq1  9449  oieq2  9450  ordtypecbv  9454  ordtypelem3  9457  zorn2lem1  10433  zorn2g  10440  cidfval  17557  cidval  17558  cidpropd  17591  lubfval  18240  glbfval  18253  grpinvfval  18790  grpinvfvalALT  18791  pj1fval  19477  mpfrcl  21498  evlsval  21499  q1pval  25521  ig1pval  25540  scutval  27142  mirval  27600  midf  27721  ismidb  27723  lmif  27730  islmib  27732  gidval  29457  grpoinvfval  29467  pjhfval  30341  cvmliftlem5  33886  cvmliftlem15  33895  trlfset  38626  dicffval  39640  dicfval  39641  dihffval  39696  dihfval  39697  hvmapffval  40224  hvmapfval  40225  hdmap1fval  40262  hdmapffval  40292  hdmapfval  40293  hgmapfval  40352  wessf1ornlem  43410
  Copyright terms: Public domain W3C validator