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

Theorem riotaeqbidv 6838
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 6837 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6836 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2840 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  crio 6834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-uni 4631  df-iota 6064  df-riota 6835
This theorem is referenced by:  dfoi  8655  oieq1  8656  oieq2  8657  ordtypecbv  8661  ordtypelem3  8664  zorn2lem1  9603  zorn2g  9610  cidfval  16541  cidval  16542  cidpropd  16574  lubfval  17183  glbfval  17196  grpinvfval  17665  pj1fval  18308  mpfrcl  19726  evlsval  19727  q1pval  24127  ig1pval  24146  mirval  25764  midf  25882  ismidb  25884  lmif  25891  islmib  25893  gidval  27695  grpoinvfval  27705  pjhfval  28583  cvmliftlem5  31594  cvmliftlem15  31603  scutval  32232  trlfset  35941  dicffval  36955  dicfval  36956  dihffval  37011  dihfval  37012  hvmapffval  37539  hvmapfval  37540  hdmap1fval  37577  hdmapffval  37607  hdmapfval  37608  hgmapfval  37667  wessf1ornlem  39860
  Copyright terms: Public domain W3C validator