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

Theorem oveqdr 7173
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 7162 . 2 (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
32adantr 481 1 ((𝜑𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  (class class class)co 7145
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-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  fullresc  17109  fucpropd  17235  resssetc  17340  resscatc  17353  issstrmgm  17851  gsumpropd  17876  grpsubpropd  18142  sylow2blem2  18675  isringd  19264  prdsringd  19291  prdscrngd  19292  prds1  19293  pwsco1rhm  19419  pwsco2rhm  19420  pwsdiagrhm  19498  primefld  19513  sralmod  19888  sralmod0  19889  issubrngd2  19890  isdomn  19995  sraassa  20027  opsrcrng  20196  opsrassa  20197  ply1lss  20292  ply1subrg  20293  opsr0  20314  opsr1  20315  subrgply1  20329  opsrring  20341  opsrlmod  20342  ply1mpl0  20351  ply1mpl1  20353  ply1ascl  20354  coe1tm  20369  evls1rhm  20413  evl1rhm  20423  evl1expd  20436  znzrh  20617  zncrng  20619  phlssphl  20731  mat0  20954  matinvg  20955  matlmod  20966  scmatsrng1  21060  1mavmul  21085  mat2pmatmul  21267  ressprdsds  22908  nmpropd  23130  tng0  23179  tngngp2  23188  tnggrpr  23191  tngnrg  23210  sranlm  23220  pi1addval  23579  cvsi  23661  tcphphl  23757  istrkgc  26167  istrkgb  26168  abvpropd2  30566  resv0g  30836  resvcmn  30838  sra1r  30885  sraring  30886  sradrng  30887  srasubrg  30888  drgextlsp  30895  tnglvec  30909  tngdim  30910  matdim  30912  fedgmullem2  30925  zhmnrg  31107  prdsbnd  34952  prdstotbnd  34953  prdsbnd2  34954  erngdvlem3  38006  erngdvlem3-rN  38014  hlhils0  38961  hlhils1N  38962  hlhillvec  38967  hlhildrng  38968  hlhil0  38971  hlhillsm  38972  mendval  39661  issubmgm2  43934  rnghmval  44090  lidlmmgm  44124  rnghmsubcsetclem1  44174  rnghmsubcsetclem2  44175  rngcifuestrc  44196  rhmsubcsetclem1  44220  rhmsubcsetclem2  44221  rhmsubcrngclem1  44226  rhmsubcrngclem2  44227
  Copyright terms: Public domain W3C validator