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

Theorem riotaeqbidv 7371
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 7370 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 7369 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2771 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1540  crio 7367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909  df-iota 6495  df-riota 7368
This theorem is referenced by:  dfoi  9510  oieq1  9511  oieq2  9512  ordtypecbv  9516  ordtypelem3  9519  zorn2lem1  10495  zorn2g  10502  cidfval  17625  cidval  17626  cidpropd  17659  lubfval  18308  glbfval  18321  grpinvfval  18900  grpinvfvalALT  18901  pj1fval  19604  mpfrcl  21868  evlsval  21869  q1pval  25907  ig1pval  25926  scutval  27539  mirval  28174  midf  28295  ismidb  28297  lmif  28304  islmib  28306  gidval  30033  grpoinvfval  30043  pjhfval  30917  cvmliftlem5  34579  cvmliftlem15  34588  trlfset  39335  dicffval  40349  dicfval  40350  dihffval  40405  dihfval  40406  hvmapffval  40933  hvmapfval  40934  hdmap1fval  40971  hdmapffval  41001  hdmapfval  41002  hgmapfval  41061  wessf1ornlem  44183
  Copyright terms: Public domain W3C validator