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

Theorem oveqdr 6628
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 6621 . 2 (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
32adantr 481 1 ((𝜑𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  (class class class)co 6604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607
This theorem is referenced by:  fullresc  16432  fucpropd  16558  resssetc  16663  resscatc  16676  issstrmgm  17173  gsumpropd  17193  grpsubpropd  17441  sylow2blem2  17957  isringd  18506  prdsringd  18533  prdscrngd  18534  prds1  18535  pwsco1rhm  18659  pwsco2rhm  18660  pwsdiagrhm  18734  sralmod  19106  sralmod0  19107  issubrngd2  19108  isdomn  19213  sraassa  19244  opsrcrng  19407  opsrassa  19408  ply1lss  19485  ply1subrg  19486  opsr0  19507  opsr1  19508  subrgply1  19522  opsrring  19534  opsrlmod  19535  ply1mpl0  19544  ply1mpl1  19546  ply1ascl  19547  coe1tm  19562  evls1rhm  19606  evl1rhm  19615  evl1expd  19628  znzrh  19810  zncrng  19812  mat0  20142  matinvg  20143  matlmod  20154  scmatsrng1  20248  1mavmul  20273  mat2pmatmul  20455  ressprdsds  22086  nmpropd  22308  tng0  22357  tngngp2  22366  tnggrpr  22369  tngnrg  22388  sranlm  22398  tchphl  22934  istrkgc  25253  istrkgb  25254  abvpropd2  29434  resv0g  29618  resvcmn  29620  zhmnrg  29790  prdsbnd  33221  prdstotbnd  33222  prdsbnd2  33223  erngdvlem3  35755  erngdvlem3-rN  35763  hlhils0  36714  hlhils1N  36715  hlhillvec  36720  hlhildrng  36721  hlhil0  36724  hlhillsm  36725  mendval  37231  issubmgm2  41075  rnghmval  41176  lidlmmgm  41210  rnghmsubcsetclem1  41260  rnghmsubcsetclem2  41261  rngcifuestrc  41282  rhmsubcsetclem1  41306  rhmsubcsetclem2  41307  rhmsubcrngclem1  41312  rhmsubcrngclem2  41313
  Copyright terms: Public domain W3C validator