Theorem oveq1 5697

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq1	⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1

Step	Hyp	Ref	Expression
1		opeq1 3644	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5344	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5693	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5693	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2152	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1296  ⟨cop 3469  ‘cfv 5049  (class class class)co 5690

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693

This theorem is referenced by:  oveq12  5699  oveq1i  5700  oveq1d  5705  rspceov  5729  fovcl  5788  ovmpt2s  5806  ov2gf  5807  ovi3  5819  caovclg  5835  caovcomg  5838  caovassg  5841  caovcang  5844  caovcan  5847  caovordig  5848  caovordg  5850  caovord  5854  caovdig  5857  caovdirg  5860  caovimo  5876  grpridd  5879  suppssov1  5891  off  5906  omcl  6262  oeicl  6263  omv2  6266  nnm0r  6280  nnacom  6285  nndi  6287  nnmass  6288  nnmsucr  6289  nnmcom  6290  nnaword  6310  nnmord  6316  nnm00  6328  eroveu  6423  th3qlem2  6435  th3q  6437  ecovcom  6439  ecovicom  6440  ecovass  6441  ecoviass  6442  ecovdi  6443  ecovidi  6444  map0g  6485  addcmpblnq  7023  addclnq  7031  mulclnq  7032  mulidnq  7045  recexnq  7046  recmulnqg  7047  ltanqg  7056  ltmnqg  7057  ltexnqq  7064  enq0ref  7089  enq0tr  7090  addcmpblnq0  7099  mulnnnq0  7106  addclnq0  7107  mulclnq0  7108  distrnq0  7115  mulcomnq0  7116  addassnq0  7118  prarloclemlo  7150  prarloclem3  7153  prarloclem5  7156  prarloclemcalc  7158  genipv  7165  genpassl  7180  genpassu  7181  addlocprlemeq  7189  distrlem4prl  7240  distrlem4pru  7241  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  prplnqu  7276  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlemladdfl  7311  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  cauappcvgprlemlim  7317  cauappcvgpr  7318  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemml  7350  caucvgprpr  7368  mulcmpblnrlemg  7383  addclsr  7396  mulclsr  7397  0idsr  7410  1idsr  7411  00sr  7412  ltasrg  7413  recexgt0sr  7416  mulgt0sr  7420  mulextsr1  7423  prsrriota  7430  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  pitonn  7482  peano2nnnn  7487  axaddrcl  7499  axmulrcl  7501  axaddcom  7502  ax1rid  7509  ax0id  7510  axprecex  7512  axcnre  7513  axpre-ltadd  7518  axpre-mulgt0  7519  axpre-mulext  7520  rereceu  7521  peano5nnnn  7524  axcaucvglemcau  7530  axcaucvglemres  7531  mulid1  7582  cnegexlem1  7754  cnegexlem2  7755  cnegex  7757  addcan2  7760  subval  7771  addlsub  7945  apreim  8177  recexap  8219  receuap  8235  divvalap  8238  cju  8519  peano2nn  8532  nn1m1nn  8538  nn1suc  8539  nnsub  8559  fv0p1e1  8635  nnm1nn0  8812  zdiv  8933  zneo  8946  nneoor  8947  zeo  8950  peano5uzti  8953  nn0ind-raph  8962  uzind4s  9177  uzind4s2  9178  qmulz  9207  cnref1o  9232  nn0ledivnn  9337  xaddnemnf  9423  xaddnepnf  9424  xaddcom  9427  xaddid1  9428  xnn0xadd0  9433  xaddass  9435  xpncan  9437  xleadd1a  9439  xltadd1  9442  xlt2add  9446  xsubge0  9447  xposdif  9448  xlesubadd  9449  xleaddadd  9453  fzsuc2  9642  fzm1  9663  fzoval  9708  exbtwnzlemstep  9808  exbtwnzlemshrink  9809  exbtwnzlemex  9810  exbtwnz  9811  rebtwn2zlemstep  9813  rebtwn2zlemshrink  9814  rebtwn2z  9815  flqlelt  9832  flqbi  9846  fldiv4p1lem1div2  9861  modqval  9880  modqadd1  9917  modqmuladd  9922  modqmuladdnn0  9924  modqm1p1mod0  9931  modqmul1  9933  modfzo0difsn  9951  addmodlteq  9954  frec2uzzd  9956  frec2uzsucd  9957  frec2uzrand  9961  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgg  9972  frecuzrdgdom  9974  frecuzrdgfun  9976  frecuzrdgsuctlem  9979  frecuzrdgsuct  9980  uzsinds  9997  iseqvalcbv  10012  seq3val  10013  seqf  10015  seq3p1  10016  seq3fveq2  10019  seq3shft2  10023  monoord  10026  monoord2  10027  seq3split  10029  seq3caopr3  10031  seq3caopr2  10032  iseqf1olemqval  10037  iseqf1olemqk  10044  seq3id2  10059  seq3homo  10060  seq3z  10061  seq3distr  10063  m1expcl2  10092  mulexp  10109  expadd  10112  expmul  10115  sq0i  10161  sqoddm1div8  10221  facp1  10253  faclbnd  10264  faclbnd3  10266  bcval  10272  bcn1  10281  bcval5  10286  bcpasc  10289  bccl  10290  hashfz1  10306  omgadd  10325  hashfzo  10345  hashfzp1  10347  hashxp  10349  seq3coll  10362  shftlem  10365  shftfvalg  10367  shftfibg  10369  shftfval  10370  shftfib  10372  shftfn  10373  shftf  10379  2shfti  10380  shftvalg  10385  shftval4g  10386  cjval  10394  imval  10399  cjexp  10442  cnrecnv  10459  cvg1nlemcau  10532  cvg1nlemres  10533  resqrexlemcalc3  10564  resqrexlemex  10573  rsqrmo  10575  resqrtcl  10577  rersqrtthlem  10578  sqrtsq  10592  absexp  10627  recan  10657  climshft  10847  climcn1  10851  climcn2  10852  subcn2  10854  fsumshft  10987  fisum0diag2  10990  fsumiun  11020  binomlem  11026  binom  11027  bcxmas  11032  isumsplit  11034  arisum2  11042  trireciplem  11043  trirecip  11044  geolim  11054  cvgratnnlemnexp  11067  cvgratnnlemmn  11068  ef0lem  11099  efval  11100  efne0  11117  efexp  11121  demoivreALT  11212  dvdsval2  11226  dvds0lem  11233  dvds1lem  11234  dvds2lem  11235  dvdsmulc  11251  divconjdvds  11277  odd2np1lem  11299  odd2np1  11300  ltoddhalfle  11320  halfleoddlt  11321  nn0o1gt2  11332  nn0o  11334  divalglemnn  11345  divalglemeunn  11348  divalglemex  11349  divalglemeuneg  11350  flodddiv4  11361  gcdabs1  11407  gcddiv  11435  dvdssqim  11440  rpmulgcd  11442  bezoutr1  11449  dvdslcm  11478  lcmeq0  11480  lcmdvds  11488  divgcdcoprm0  11510  prmind2  11529  isprm6  11553  rpexp  11559  sqrt2irr  11568  pw2dvdslemn  11570  pw2dvdseu  11573  oddpwdclemxy  11574  nn0gcdsq  11605  phicl2  11617  phibndlem  11619  hashdvds  11624  crth  11627  phimullem  11628  hashgcdlem  11630  psmettri2  12114  isxmet2d  12134  xmeteq0  12145  xmettri2  12147  metrest  12292  cncfval  12325  mulc1cncf  12342  addccncf  12349  mulcncf  12354  expcncf  12355  qdencn  12620