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

Theorem oveqdr 7179
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 7168 . 2 (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
32adantr 481 1 ((𝜑𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  (class class class)co 7151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-rex 3148  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154
This theorem is referenced by:  fullresc  17113  fucpropd  17239  resssetc  17344  resscatc  17357  issstrmgm  17854  gsumpropd  17879  grpsubpropd  18136  sylow2blem2  18668  isringd  19257  prdsringd  19284  prdscrngd  19285  prds1  19286  pwsco1rhm  19412  pwsco2rhm  19413  pwsdiagrhm  19491  primefld  19506  sralmod  19881  sralmod0  19882  issubrngd2  19883  isdomn  19988  sraassa  20020  opsrcrng  20188  opsrassa  20189  ply1lss  20281  ply1subrg  20282  opsr0  20303  opsr1  20304  subrgply1  20318  opsrring  20330  opsrlmod  20331  ply1mpl0  20340  ply1mpl1  20342  ply1ascl  20343  coe1tm  20358  evls1rhm  20402  evl1rhm  20411  evl1expd  20424  znzrh  20605  zncrng  20607  phlssphl  20719  mat0  20942  matinvg  20943  matlmod  20954  scmatsrng1  21048  1mavmul  21073  mat2pmatmul  21255  ressprdsds  22896  nmpropd  23118  tng0  23167  tngngp2  23176  tnggrpr  23179  tngnrg  23198  sranlm  23208  pi1addval  23567  cvsi  23649  tcphphl  23745  istrkgc  26154  istrkgb  26155  abvpropd2  30553  resv0g  30823  resvcmn  30825  sra1r  30872  sraring  30873  sradrng  30874  srasubrg  30875  drgextlsp  30882  tnglvec  30896  tngdim  30897  matdim  30899  fedgmullem2  30912  zhmnrg  31094  prdsbnd  34939  prdstotbnd  34940  prdsbnd2  34941  erngdvlem3  37993  erngdvlem3-rN  38001  hlhils0  38948  hlhils1N  38949  hlhillvec  38954  hlhildrng  38955  hlhil0  38958  hlhillsm  38959  mendval  39644  issubmgm2  43885  rnghmval  43990  lidlmmgm  44024  rnghmsubcsetclem1  44074  rnghmsubcsetclem2  44075  rngcifuestrc  44096  rhmsubcsetclem1  44120  rhmsubcsetclem2  44121  rhmsubcrngclem1  44126  rhmsubcrngclem2  44127
  Copyright terms: Public domain W3C validator