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

Theorem oveq1 5749
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq1  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )

Proof of Theorem oveq1
StepHypRef Expression
1 opeq1 3675 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21fveq2d 5393 . 2  |-  ( A  =  B  ->  ( F `  <. A ,  C >. )  =  ( F `  <. B ,  C >. ) )
3 df-ov 5745 . 2  |-  ( A F C )  =  ( F `  <. A ,  C >. )
4 df-ov 5745 . 2  |-  ( B F C )  =  ( F `  <. B ,  C >. )
52, 3, 43eqtr4g 2175 1  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
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  oveq1i  5752  oveq1d  5757  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  grpridd  5935  suppssov1  5947  off  5962  omcl  6325  oeicl  6326  omv2  6329  nnm0r  6343  nnacom  6348  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  nnaword  6375  nnmord  6381  nnm00  6393  eroveu  6488  th3qlem2  6500  th3q  6502  ecovcom  6504  ecovicom  6505  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  map0g  6550  addcmpblnq  7143  addclnq  7151  mulclnq  7152  mulidnq  7165  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  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  prarloclemcalc  7278  genipv  7285  genpassl  7300  genpassu  7301  addlocprlemeq  7309  distrlem4prl  7360  distrlem4pru  7361  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  prplnqu  7396  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  cauappcvgpr  7438  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemml  7470  caucvgprpr  7488  mulcmpblnrlemg  7516  addclsr  7529  mulclsr  7530  0idsr  7543  1idsr  7544  00sr  7545  ltasrg  7546  recexgt0sr  7549  mulgt0sr  7554  mulextsr1  7557  prsrriota  7564  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  pitonn  7624  peano2nnnn  7629  axaddrcl  7641  axmulrcl  7643  axaddcom  7646  ax1rid  7653  ax0id  7654  axprecex  7656  axcnre  7657  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  rereceu  7665  peano5nnnn  7668  axcaucvglemcau  7674  axcaucvglemres  7675  mulid1  7731  cnegexlem1  7905  cnegexlem2  7906  cnegex  7908  addcan2  7911  subval  7922  addlsub  8100  apreim  8332  recexap  8381  receuap  8397  divvalap  8401  cju  8683  peano2nn  8696  nn1m1nn  8702  nn1suc  8703  nnsub  8723  fv0p1e1  8799  nnm1nn0  8976  zdiv  9097  zneo  9110  nneoor  9111  zeo  9114  peano5uzti  9117  nn0ind-raph  9126  uzind4s  9341  uzind4s2  9342  qmulz  9371  cnref1o  9396  nn0ledivnn  9509  xaddnemnf  9595  xaddnepnf  9596  xaddcom  9599  xaddid1  9600  xnn0xadd0  9605  xaddass  9607  xpncan  9609  xleadd1a  9611  xltadd1  9614  xlt2add  9618  xsubge0  9619  xposdif  9620  xlesubadd  9621  xleaddadd  9625  fzsuc2  9814  fzm1  9835  fzoval  9880  exbtwnzlemstep  9980  exbtwnzlemshrink  9981  exbtwnzlemex  9982  exbtwnz  9983  rebtwn2zlemstep  9985  rebtwn2zlemshrink  9986  rebtwn2z  9987  flqlelt  10004  flqbi  10018  fldiv4p1lem1div2  10033  modqval  10052  modqadd1  10089  modqmuladd  10094  modqmuladdnn0  10096  modqm1p1mod0  10103  modqmul1  10105  modfzo0difsn  10123  addmodlteq  10126  frec2uzzd  10128  frec2uzsucd  10129  frec2uzrand  10133  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgdom  10146  frecuzrdgfun  10148  frecuzrdgsuctlem  10151  frecuzrdgsuct  10152  uzsinds  10170  iseqvalcbv  10185  seq3val  10186  seqvalcd  10187  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3fveq2  10197  seq3shft2  10201  monoord  10204  monoord2  10205  seq3split  10207  seq3caopr3  10209  seq3caopr2  10210  iseqf1olemqval  10215  iseqf1olemqk  10222  seq3id2  10237  seq3homo  10238  seq3z  10239  seq3distr  10241  m1expcl2  10270  mulexp  10287  expadd  10290  expmul  10293  sq0i  10339  sqoddm1div8  10399  facp1  10431  faclbnd  10442  faclbnd3  10444  bcval  10450  bcn1  10459  bcval5  10464  bcpasc  10467  bccl  10468  hashfz1  10484  omgadd  10503  hashfzo  10523  hashfzp1  10525  hashxp  10527  seq3coll  10540  shftlem  10543  shftfvalg  10545  shftfibg  10547  shftfval  10548  shftfib  10550  shftfn  10551  shftf  10557  2shfti  10558  shftvalg  10563  shftval4g  10564  cjval  10572  imval  10577  cjexp  10620  cnrecnv  10637  cvg1nlemcau  10711  cvg1nlemres  10712  resqrexlemcalc3  10743  resqrexlemex  10752  rsqrmo  10754  resqrtcl  10756  rersqrtthlem  10757  sqrtsq  10771  absexp  10806  recan  10836  climshft  11028  climcn1  11032  climcn2  11033  subcn2  11035  fsumshft  11168  fisum0diag2  11171  fsumiun  11201  binomlem  11207  binom  11208  bcxmas  11213  isumsplit  11215  arisum2  11223  trireciplem  11224  trirecip  11225  geolim  11235  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  ef0lem  11280  efval  11281  efne0  11298  efexp  11302  demoivreALT  11394  dvdsval2  11408  dvds0lem  11415  dvds1lem  11416  dvds2lem  11417  dvdsmulc  11433  divconjdvds  11459  odd2np1lem  11481  odd2np1  11482  ltoddhalfle  11502  halfleoddlt  11503  nn0o1gt2  11514  nn0o  11516  divalglemnn  11527  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  flodddiv4  11543  gcdabs1  11589  gcddiv  11619  dvdssqim  11624  rpmulgcd  11626  bezoutr1  11633  dvdslcm  11662  lcmeq0  11664  lcmdvds  11672  divgcdcoprm0  11694  prmind2  11713  isprm6  11737  rpexp  11743  sqrt2irr  11752  pw2dvdslemn  11754  pw2dvdseu  11757  oddpwdclemxy  11758  nn0gcdsq  11789  phicl2  11801  phibndlem  11803  hashdvds  11808  crth  11811  phimullem  11812  hashgcdlem  11814  ennnfonelemr  11847  ctinfom  11852  cnmptcom  12378  psmettri2  12408  isxmet2d  12428  xmeteq0  12439  xmettri2  12441  metrest  12586  cncfval  12639  mulc1cncf  12656  addccncf  12666  mulcncf  12671  expcncf  12672  limccnp2lem  12725  dvcnp2cntop  12743  dvcoapbr  12751  dvexp  12755  dvrecap  12757  dvef  12767  sincn  12769  coscn  12770  ptolemy  12816  qdencn  13118  isomninn  13122
  Copyright terms: Public domain W3C validator