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

Theorem oveqdr 7386
Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
Hypothesis
Ref Expression
oveqdr.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
oveqdr ((𝜑𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Proof of Theorem oveqdr
StepHypRef Expression
1 oveqdr.1 . . 3 (𝜑𝐹 = 𝐺)
21oveqd 7375 . 2 (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
32adantr 482 1 ((𝜑𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  fullresc  17738  fucpropd  17867  resssetc  17979  resscatc  17996  issstrmgm  18509  gsumpropd  18534  grpsubpropd  18853  sylow2blem2  19404  isringd  20010  prdsringd  20037  prdscrngd  20038  prds1  20039  pwsco1rhm  20173  pwsco2rhm  20174  pwsdiagrhm  20259  primefld  20275  sralmod  20659  sralmod0  20660  issubrngd2  20661  isdomn  20767  znzrh  20952  zncrng  20954  phlssphl  21066  sraassa  21276  opsrcrng  21469  opsrassa  21470  ply1lss  21570  ply1subrg  21571  opsr0  21592  opsr1  21593  subrgply1  21607  opsrring  21619  opsrlmod  21620  ply1mpl0  21629  ply1mpl1  21631  ply1ascl  21632  coe1tm  21647  evls1rhm  21691  evl1rhm  21701  evl1expd  21714  mat0  21769  matinvg  21770  matlmod  21781  scmatsrng1  21875  1mavmul  21900  mat2pmatmul  22083  ressprdsds  23727  nmpropd  23953  tng0  24005  tngngp2  24019  tnggrpr  24022  tngnrg  24041  sranlm  24051  pi1addval  24414  cvsi  24496  tcphphl  24594  istrkgc  27399  istrkgb  27400  abvpropd2  31822  resv0g  32135  resvcmn  32137  sra1r  32288  sraring  32289  sradrng  32290  srasubrg  32291  drgextlsp  32298  tnglvec  32312  tngdim  32313  matdim  32315  fedgmullem2  32328  zhmnrg  32551  prdsbnd  36255  prdstotbnd  36256  prdsbnd2  36257  erngdvlem3  39456  erngdvlem3-rN  39464  hlhils0  40415  hlhils1N  40416  hlhillvec  40421  hlhildrng  40422  hlhil0  40425  hlhillsm  40426  mendval  41513  mnring0gd  42506  mnringlmodd  42513  issubmgm2  46091  rnghmval  46196  lidlmmgm  46230  rnghmsubcsetclem1  46280  rnghmsubcsetclem2  46281  rngcifuestrc  46302  rhmsubcsetclem1  46326  rhmsubcsetclem2  46327  rhmsubcrngclem1  46332  rhmsubcrngclem2  46333
  Copyright terms: Public domain W3C validator