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

Theorem riotaeqbidv 6776
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 6775 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 6774 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2808 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1634  crio 6772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rex 3070  df-uni 4586  df-iota 6005  df-riota 6773
This theorem is referenced by:  dfoi  8593  oieq1  8594  oieq2  8595  ordtypecbv  8599  ordtypelem3  8602  zorn2lem1  9541  zorn2g  9548  cidfval  16564  cidval  16565  cidpropd  16597  lubfval  17206  glbfval  17219  grpinvfval  17688  pj1fval  18334  mpfrcl  19753  evlsval  19754  q1pval  24154  ig1pval  24173  mirval  25792  midf  25910  ismidb  25912  lmif  25919  islmib  25921  gidval  27723  grpoinvfval  27733  pjhfval  28612  cvmliftlem5  31626  cvmliftlem15  31635  scutval  32265  trlfset  35985  dicffval  36999  dicfval  37000  dihffval  37055  dihfval  37056  hvmapffval  37583  hvmapfval  37584  hdmap1fval  37621  hdmapffval  37651  hdmapfval  37652  hgmapfval  37711  wessf1ornlem  39902
  Copyright terms: Public domain W3C validator