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

Theorem riotaeqbidv 6574
 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 6573 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6572 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2655 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480  ℩crio 6570 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4408  df-iota 5815  df-riota 6571 This theorem is referenced by:  dfoi  8368  oieq1  8369  oieq2  8370  ordtypecbv  8374  ordtypelem3  8377  zorn2lem1  9270  zorn2g  9277  cidfval  16269  cidval  16270  cidpropd  16302  lubfval  16910  glbfval  16923  grpinvfval  17392  pj1fval  18039  mpfrcl  19450  evlsval  19451  q1pval  23834  ig1pval  23853  mirval  25467  midf  25585  ismidb  25587  lmif  25594  islmib  25596  gidval  27236  grpoinvfval  27246  pjhfval  28125  cvmliftlem5  31014  cvmliftlem15  31023  trlfset  34962  dicffval  35978  dicfval  35979  dihffval  36034  dihfval  36035  hvmapffval  36562  hvmapfval  36563  hdmap1fval  36601  hdmapffval  36633  hdmapfval  36634  hgmapfval  36693  wessf1ornlem  38876
 Copyright terms: Public domain W3C validator