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

Theorem riotaeqbidv 6868
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 6867 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6866 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2860 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1658  crio 6864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rex 3122  df-uni 4658  df-iota 6085  df-riota 6865
This theorem is referenced by:  dfoi  8684  oieq1  8685  oieq2  8686  ordtypecbv  8690  ordtypelem3  8693  zorn2lem1  9632  zorn2g  9639  cidfval  16688  cidval  16689  cidpropd  16721  lubfval  17330  glbfval  17343  grpinvfval  17813  pj1fval  18457  mpfrcl  19877  evlsval  19878  q1pval  24311  ig1pval  24330  mirval  25966  midf  26084  ismidb  26086  lmif  26093  islmib  26095  gidval  27921  grpoinvfval  27931  pjhfval  28809  cvmliftlem5  31816  cvmliftlem15  31825  scutval  32449  trlfset  36234  dicffval  37248  dicfval  37249  dihffval  37304  dihfval  37305  hvmapffval  37832  hvmapfval  37833  hdmap1fval  37870  hdmapffval  37900  hdmapfval  37901  hgmapfval  37960  wessf1ornlem  40178
  Copyright terms: Public domain W3C validator