ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq2 GIF version

Theorem oveq2 5750
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3676 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5393 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5745 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5745 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2175 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  cop 3500  cfv 5093  (class class class)co 5742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  oveq12  5751  oveq2i  5753  oveq2d  5758  ovanraleqv  5766  rspceov  5781  fovcl  5844  ovmpos  5862  ov2gf  5863  ovi3  5875  caovclg  5891  caovcomg  5894  caovassg  5897  caovcang  5900  caovcan  5903  caovordig  5904  caovordg  5906  caovord  5910  caovdig  5913  caovdirg  5916  caovimo  5932  grprinvlem  5933  grprinvd  5934  suppssov1  5947  off  5962  omv  6319  oeiv  6320  oasuc  6328  oawordriexmid  6334  omsuc  6336  nna0r  6342  nnm0r  6343  nnacl  6344  nnmcl  6345  nnacom  6348  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  nnaordi  6372  nnaord  6373  nnmordi  6380  nnmord  6381  nnaordex  6391  nnawordex  6392  nnm00  6393  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem2  6500  th3q  6502  ecovcom  6504  ecovicom  6505  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  addcanpig  7110  mulcanpig  7111  addcmpblnq  7143  addclnq  7151  mulclnq  7152  recexnq  7166  recmulnqg  7167  ltanqg  7176  ltmnqg  7177  ltexnqq  7184  enq0ref  7209  enq0tr  7210  addcmpblnq0  7219  mulnnnq0  7226  addclnq0  7227  mulclnq0  7228  distrnq0  7235  mulcomnq0  7236  addassnq0  7238  nq02m  7241  prarloclem3  7273  genipv  7285  genpassl  7300  genpassu  7301  addlocpr  7312  distrlem1prl  7358  distrlem1pru  7359  1idprl  7366  1idpru  7367  ltexprlemell  7374  ltexprlemelu  7375  ltexpri  7389  lteupri  7393  ltaprlem  7394  recexprlem1ssl  7409  recexprlem1ssu  7410  recexpr  7414  cauappcvgprlemm  7421  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  cauappcvgpr  7438  mulcmpblnrlemg  7516  addclsr  7529  mulclsr  7530  ltasrg  7546  negexsr  7548  recexgt0sr  7549  mulgt0sr  7554  mulextsr1  7557  srpospr  7559  caucvgsrlemgt1  7571  map2psrprg  7581  axaddrcl  7641  axmulrcl  7643  axaddcom  7646  axrnegex  7655  axprecex  7656  axcnre  7657  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  rereceu  7665  recriota  7666  axcaucvglemres  7675  readdcan  7870  cnegexlem1  7905  cnegex  7908  addcan  7910  negeq  7923  subadd  7933  addid0  8103  ine0  8124  rimul  8315  cru  8332  apreim  8333  recexap  8382  mulcanapd  8390  receuap  8398  divmulap  8403  cju  8687  nnaddcl  8708  nnmulcl  8709  nnsub  8727  nnnn0addcl  8975  zaddcllempos  9059  zaddcl  9062  zdiv  9107  deceq1  9154  deceq2  9155  uzaddcl  9349  zq  9386  qreccl  9402  cnref1o  9408  xaddnemnf  9608  xaddnepnf  9609  xaddcom  9612  xnn0xadd0  9618  xnegdi  9619  xaddass  9620  xlt2add  9631  xlesubadd  9634  xleaddadd  9638  fzsuc2  9827  fzrevral  9853  fzshftral  9856  2ffzeq  9886  exfzdc  9985  exbtwnzlemshrink  9994  rebtwn2zlemshrink  9999  modqval  10065  modqmuladd  10107  modqmuladdnn0  10109  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  frecuzrdgsuctlem  10164  frecfzennn  10167  uzsinds  10183  iseqvalcbv  10198  seq3val  10199  seqvalcd  10200  seqovcd  10204  seq3caopr3  10222  seq3caopr2  10223  seq3f1olemp  10243  seq3id  10249  seq3homo  10251  seq3z  10252  seq3distr  10254  expp1  10268  expnegap0  10269  expcllem  10272  expcl2lemap  10273  m1expcl2  10283  expap0  10291  mulexp  10300  expadd  10303  expmul  10306  leexp2r  10315  leexp1a  10316  bernneq  10380  expnbnd  10383  expcan  10431  facdiv  10452  faclbnd3  10457  faclbnd6  10458  bcval  10463  bcpasc  10480  bccl  10481  fz1eqb  10505  omgadd  10516  hashunlem  10518  hashfzo  10536  hashfzp1  10538  shftfvalg  10558  shftfval  10561  cjth  10586  remim  10600  reim0b  10602  cjexp  10633  cnrecnv  10650  cvg1nlemcau  10724  cvg1nlemres  10725  recvguniq  10735  resqrexlemp1rp  10746  resqrexlemfp1  10749  resqrexlemlo  10753  resqrexlemgt0  10760  resqrexlemoverl  10761  resqrexlemglsq  10762  resqrexlemsqa  10764  resqrexlemex  10765  resqrex  10766  absexp  10819  recan  10849  climcn2  11046  subcn2  11048  summodc  11120  fsum3  11124  fsum3cvg3  11133  fsumrev  11180  fisum0diag2  11184  telfsumo  11203  fsumrelem  11208  binomlem  11220  binom  11221  binom1dif  11224  bcxmaslem1  11225  bcxmas  11226  isumshft  11227  divcnv  11234  arisum  11235  trireciplem  11237  expcnvap0  11239  expcnvre  11240  expcnv  11241  explecnv  11242  geosergap  11243  geolim  11248  geolim2  11249  geo2sum  11251  geo2lim  11253  geoisum  11254  geoisumr  11255  geoisum1  11256  geoisum1c  11257  cvgratnnlemsumlt  11265  cvgratz  11269  eftvalcn  11290  efcvgfsum  11300  ege2le3  11304  efcj  11306  efaddlem  11307  efexp  11315  eftlub  11323  efgt1p2  11328  eflegeo  11335  sinval  11336  cosval  11337  demoivreALT  11407  divides  11422  dvdscmul  11447  dvds2ln  11453  dvdstr  11457  odd2np1lem  11496  odd2np1  11497  2tp1odd  11508  opeo  11521  omeo  11522  m1expe  11523  m1expo  11524  m1exp1  11525  divalglemnn  11542  divalglemeunn  11545  divalglemeuneg  11547  divalgmod  11551  ndvdssub  11554  gcd0id  11594  bezoutlemnewy  11611  bezoutlema  11614  bezoutlemb  11615  bezoutlemex  11616  bezoutlemaz  11618  bezoutlembz  11619  gcdmultiple  11635  gcdmultiplez  11636  dvdsmulgcd  11640  rplpwr  11642  nn0seqcvgd  11649  dvdslcm  11677  lcmeq0  11679  lcmcl  11680  lcmneg  11682  lcmgcdlem  11685  lcmdvds  11687  lcmid  11688  lcmgcdeq  11691  coprmdvds  11700  mulgcddvds  11702  qredeq  11704  cncongr1  11711  cncongr2  11712  cncongrcoprm  11714  prmind2  11728  isprm6  11752  prmdvdsexp  11753  prmdvdsexpr  11755  sqrt2irr  11767  pw2dvdslemn  11770  pw2dvdseu  11773  oddpwdclemxy  11774  sqpweven  11780  2sqpwodd  11781  sqne2sq  11782  nn0gcdsq  11805  qden1elz  11810  phival  11816  dfphi2  11823  ennnfonelemnn0  11862  ennnfonelemr  11863  txdis1cn  12374  cnmptcom  12394  psmettri2  12424  isxmet2d  12444  xmeteq0  12455  xmettri2  12457  elblps  12486  elbl  12487  blssps  12523  blss  12524  ssblex  12527  blin2  12528  metss2  12594  comet  12595  bdmopn  12600  txmetcnp  12614  blssioo  12641  divcnap  12651  cncfval  12655  cncfi  12661  mulc1cncf  12672  cdivcncfap  12683  mulcncf  12687  expcncf  12688  cnopnap  12690  ellimc3apf  12725  cnlimci  12738  limccnpcntop  12740  limccnp2lem  12741  reldvg  12744  eldvap  12747  dvexp  12771  dvexp2  12772  dvrecap  12773  sin0pilem2  12790  trilpolemclim  13156  trilpolemcl  13157  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161  trilpo  13163
  Copyright terms: Public domain W3C validator