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

Theorem riotaeqbidv 7106
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 7105 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 7104 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2853 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  crio 7102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rex 3141  df-uni 4831  df-iota 6307  df-riota 7103
This theorem is referenced by:  dfoi  8963  oieq1  8964  oieq2  8965  ordtypecbv  8969  ordtypelem3  8972  zorn2lem1  9906  zorn2g  9913  cidfval  16935  cidval  16936  cidpropd  16968  lubfval  17576  glbfval  17589  grpinvfval  18080  grpinvfvalALT  18081  pj1fval  18749  mpfrcl  20226  evlsval  20227  q1pval  24674  ig1pval  24693  mirval  26368  midf  26489  ismidb  26491  lmif  26498  islmib  26500  gidval  28216  grpoinvfval  28226  pjhfval  29100  cvmliftlem5  32433  cvmliftlem15  32442  scutval  33162  trlfset  37176  dicffval  38190  dicfval  38191  dihffval  38246  dihfval  38247  hvmapffval  38774  hvmapfval  38775  hdmap1fval  38812  hdmapffval  38842  hdmapfval  38843  hgmapfval  38902  wessf1ornlem  41321
  Copyright terms: Public domain W3C validator