Theorem fveq2 5198

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq2	⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 3788	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 4908	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 4930	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 4930	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2138	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1284   class class class wbr 3785  ℩cio 4885  ‘cfv 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930

This theorem is referenced by:  fveq2i  5201  fveq2d  5202  fvifdc  5217  dffn5imf  5249  fvelimab  5250  ssimaex  5255  fvmptssdm  5276  fvmptf  5284  eqfnfv2f  5290  fvelrn  5319  ralrnmpt  5330  rexrnmpt  5331  foco2  5339  ffnfvf  5345  fmptco  5351  fcompt  5354  fcoconst  5355  fnressn  5370  fressnfv  5371  fconstfvm  5400  funiunfvdmf  5424  f1veqaeq  5429  dff13f  5430  f1fveq  5432  f1elima  5433  f1ocnvfv  5439  f1ocnvfvb  5440  fcofo  5444  cocan2  5448  fliftfun  5456  isorel  5468  isocnv  5471  isotr  5476  f1oiso2  5486  ffnov  5625  eqfnov  5627  fnovim  5629  fnrnov  5666  foov  5667  funimassov  5670  ovelimab  5671  suppssfv  5728  fnofval  5741  ofrval  5742  offval2  5746  ofrfval2  5747  ofco  5749  caofinvl  5753  op1std  5795  op2ndd  5796  1stval2  5802  2ndval2  5803  unielxp  5820  reldm  5832  oprabco  5858  2ndconst  5863  f1o2ndf1  5869  mpt2xopn0yelv  5877  mpt2xopoveq  5878  smoel  5938  tfrlem1  5946  tfrlem3-2  5950  tfrlem3-2d  5951  tfrlem5  5953  tfrlem9  5958  tfr0  5960  tfrlemiubacc  5967  tfrlemi1  5969  tfrexlem  5971  tfri3  5976  rdgtfr  5984  rdgss  5993  rdgisuc1  5994  rdgisucinc  5995  rdgon  5996  frecabex  6007  frecsuclem3  6013  frecsuc  6014  frecrdg  6015  freccl  6016  oav  6057  omv  6058  oeiv  6059  dom2lem  6275  xpcomco  6323  fidceq  6354  ordiso2  6446  mulpipq2  6561  genipv  6699  genpelxp  6701  addcanprleml  6804  addcanprlemu  6805  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  cauappcvgprlemm  6835  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgprlemlim  6851  cauappcvgpr  6852  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsrlembound  6970  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemoffres  6976  caucvgsrlembnd  6977  caucvgsr  6978  axcaucvglemcau  7064  axcaucvglemres  7065  uz11  8641  cnref1o  8733  fzprval  9099  fztpval  9100  frec2uzzd  9402  frec2uzuzd  9404  frec2uzltd  9405  frec2uzlt2d  9406  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgfn  9414  frecfzennn  9419  iseqeq1  9434  iseqovex  9439  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  iseqss  9446  iseqfveq2  9448  iseqfveq  9450  iseqfeq  9451  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid3s  9466  iseqhomo  9468  iseqz  9469  serile  9474  expivallem  9477  expival  9478  facp1  9657  faccl  9662  facdiv  9665  facwordi  9667  faclbnd  9668  facubnd  9672  bcval  9676  ibcval5  9690  reval  9736  replim  9746  cj11  9792  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  rexuz3  9876  absval  9887  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrexlemsqa  9910  resqrexlemex  9911  abs00bd  9952  cau3lem  10000  caubnd2  10003  climconst  10129  climmpt  10139  climshftlemg  10141  climcn1  10147  climle  10172  climub  10182  climserile  10183  climcau  10184  climcvg1nlem  10186  climcvg1n  10187  serif0  10189  dvdsabseq  10247  dvdsfac  10260  zsupcllemex  10342  infssuzex  10345  gcd0id  10370  nn0seqcvgd  10423  ialginv  10429  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  eucalglt  10439  lcmid  10462  qredeu  10479  prmfac1  10531  sqne2sq  10555  qdencn  10785