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

Theorem riotaeqbidv 6654
 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 6653 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6652 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2685 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  ℩crio 6650 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469  df-iota 5889  df-riota 6651 This theorem is referenced by:  dfoi  8457  oieq1  8458  oieq2  8459  ordtypecbv  8463  ordtypelem3  8466  zorn2lem1  9356  zorn2g  9363  cidfval  16384  cidval  16385  cidpropd  16417  lubfval  17025  glbfval  17038  grpinvfval  17507  pj1fval  18153  mpfrcl  19566  evlsval  19567  q1pval  23958  ig1pval  23977  mirval  25595  midf  25713  ismidb  25715  lmif  25722  islmib  25724  gidval  27494  grpoinvfval  27504  pjhfval  28383  cvmliftlem5  31397  cvmliftlem15  31406  scutval  32036  trlfset  35765  dicffval  36780  dicfval  36781  dihffval  36836  dihfval  36837  hvmapffval  37364  hvmapfval  37365  hdmap1fval  37403  hdmapffval  37435  hdmapfval  37436  hgmapfval  37495  wessf1ornlem  39685
 Copyright terms: Public domain W3C validator