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

Theorem riotaeqbidv 6514
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 6513 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6512 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2644 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  crio 6510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-iota 5768  df-riota 6511
This theorem is referenced by:  dfoi  8299  oieq1  8300  oieq2  8301  ordtypecbv  8305  ordtypelem3  8308  zorn2lem1  9201  zorn2g  9208  cidfval  16160  cidval  16161  cidpropd  16193  lubfval  16801  glbfval  16814  grpinvfval  17283  pj1fval  17930  mpfrcl  19339  evlsval  19340  q1pval  23717  ig1pval  23736  mirval  25350  midf  25468  ismidb  25470  lmif  25477  islmib  25479  gidval  26750  grpoinvfval  26760  pjhfval  27639  cvmliftlem5  30525  cvmliftlem15  30534  trlfset  34465  dicffval  35481  dicfval  35482  dihffval  35537  dihfval  35538  hvmapffval  36065  hvmapfval  36066  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapfval  36196  wessf1ornlem  38366
  Copyright terms: Public domain W3C validator