Theorem fveq2 5690

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 4128	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5355	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5380	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5380	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1402   class class class wbr 4125  ℩cio 5330  ‘cfv 5372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  fveq2i  5693  fveq2d  5694  2fveq3  5695  fvifdc  5712  dffn5imf  5752  fvelimab  5753  ssimaex  5758  fvco4  5771  fvmptssdm  5784  fvmptf  5792  eqfnfv2f  5801  fvelrn  5830  ralrnmpt  5841  rexrnmpt  5842  ffnfvf  5858  fmptco  5865  cofmpt  5868  fcompt  5869  fcoconst  5870  fsn2g  5874  fnressn  5892  fressnfv  5893  fconstfvm  5924  dfimafnf  5945  foco2  5949  funiunfvdmf  5960  f1veqaeq  5965  dff13f  5966  f1fveq  5968  f1elima  5969  f1ocnvfv  5975  f1ocnvfvb  5976  fcofo  5980  cocan2  5984  fliftfun  5992  isorel  6004  isocnv  6007  isotr  6012  f1oiso2  6023  canth  6026  imbrov2fvoveq  6100  ffnov  6182  eqfnov  6185  fnovim  6187  fnrnov  6225  foov  6226  funimassov  6229  ovelimab  6230  ofvalg  6302  ofrval  6303  offval2  6308  ofrfval2  6309  ofco  6311  caofinvl  6318  op1std  6372  op2ndd  6373  1stval2  6379  2ndval2  6380  unielxp  6398  reldm  6410  oprabco  6443  2ndconst  6448  f1o2ndf1  6454  elsuppfng  6472  elsuppfn  6473  mpoxopn0yelv  6500  mpoxopoveq  6501  smoel  6561  tfrlem1  6569  tfrlem3-2d  6573  tfrlem5  6575  tfrlem9  6580  tfr0dm  6583  tfrlemiubacc  6591  tfrlemi1  6593  tfrexlem  6595  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemubacc  6607  tfr1onlemaccex  6609  tfr1onlemres  6610  tfri1dALT  6612  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemubacc  6620  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  tfrcl  6625  tfri3  6628  rdgtfr  6635  rdgss  6644  rdgisuc1  6645  rdgisucinc  6646  rdgon  6647  frecabex  6659  frecabcl  6660  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  frecrdg  6669  oav  6717  omv  6718  oeiv  6719  fvixp  6975  cbvixp  6987  mptelixpg  7006  elixpsn  7007  dom2lem  7048  xpcomco  7114  xpmapen  7140  fidceq  7161  fieq0  7300  ordiso2  7365  djune  7408  updjudhcoinlf  7410  updjudhcoinrg  7411  updjud  7412  omp1eom  7425  0ct  7437  ctmlemr  7438  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  nninfninc  7453  nnnninfeq  7458  nnnninfeq2  7459  enomnilem  7468  finomni  7470  fodjuomnilemdc  7474  fodju0  7477  fodjuomni  7479  ismkvnex  7485  fodjumkv  7490  nninfwlporlemd  7502  nninfwlpor  7504  exmidaclem  7554  cc1  7621  cc2lem  7622  cc2  7623  cc3  7624  mulpipq2  7728  genipv  7866  genpelxp  7868  addcanprleml  7971  addcanprlemu  7972  recexprlemm  7981  recexprlemdisj  7987  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  cauappcvgprlemm  8002  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  cauappcvgprlemlim  8018  cauappcvgpr  8019  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprlem2  8037  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemnbj  8050  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsrlembound  8151  caucvgsrlemgt1  8152  caucvgsrlemoffval  8153  caucvgsrlemoffres  8157  caucvgsrlembnd  8158  caucvgsr  8159  axcaucvglemcau  8255  axcaucvglemres  8256  uz11  9924  cnref1o  10030  fzprval  10467  fztpval  10468  zsupcllemex  10641  infssuzex  10644  suprzubdc  10649  frec2uzuzd  10817  frec2uzltd  10818  frec2uzlt2d  10819  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgtcl  10827  frecuzrdgg  10831  frecuzrdgfunlem  10834  frecfzennn  10841  seqeq1  10865  iseqovex  10873  seq3val  10875  seqvalcd  10876  seq3-1  10877  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3clss  10886  seq3fveq2  10890  seqfveq2g  10892  seqfveqg  10893  seq3fveq  10894  seq3feq  10895  seq3shft2  10896  seqshft2g  10897  monoord  10900  monoord2  10901  ser3mono  10902  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3caopr2  10908  seqcaopr2g  10909  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqval  10915  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1olemp  10930  seq3f1oleml  10931  seq3f1o  10932  seqf1oglem2a  10933  seqf1og  10936  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  ser3ge0  10951  ser3le  10952  exp3vallem  10955  exp3val  10956  facp1  11146  faccl  11151  facdiv  11154  facwordi  11156  faclbnd  11157  facubnd  11161  bcval  11165  bcval5  11179  fz1eqb  11207  omgadd  11220  hashxp  11245  hashmap  11246  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  hashf1  11265  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  eqwrd  11323  lswwrd  11329  lswex  11334  ccatfvalfi  11338  ccatval1  11343  ccatval2  11344  ccatalpha  11359  s1eq  11365  eqs1  11374  swrdval  11398  ccatopth2  11467  wrd2ind  11473  seq3shft  11581  reval  11592  replim  11602  cj11  11649  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  rexuz3  11734  absval  11745  resqrexlemover  11754  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  resqrexlemsqa  11768  resqrexlemex  11769  abs00bd  11810  cau3lem  11858  caubnd2  11861  climconst  12034  climmpt  12044  climshftlemg  12046  climcn1  12052  climle  12078  climub  12088  climserle  12089  climcau  12091  climcvg1nlem  12093  climcvg1n  12094  serf0  12096  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  summodclem2  12127  summodc  12128  zsumdc  12129  fsum3  12132  fsumf1o  12135  fisumss  12137  fsum3cvg2  12139  fsum3ser  12142  fsumcl2lem  12143  fsumadd  12151  sumsnf  12154  isummulc2  12171  isumge0  12175  isumadd  12176  fsum2dlemstep  12179  fsummulc2  12193  fsumconst  12199  fsumrelem  12216  isumshft  12235  isum1p  12237  isumnn0nn  12238  isumrpcl  12239  isumlessdc  12241  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  clim2prod  12284  prodfap0  12290  prodfrecap  12291  prodfdivap  12292  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  prodsnf  12337  fprodfac  12360  fprodconst  12365  fprod2dlemstep  12367  eftvalcn  12402  ef0lem  12405  ege2le3  12416  efcj  12418  efaddlem  12419  eftlub  12435  efgt1p2  12440  reef11  12444  tanvalap  12453  efieq1re  12517  eirraplem  12522  dvdsabseq  12592  dvdsfac  12605  gcd0id  12734  nninfctlemfo  12795  nn0seqcvgd  12797  alginv  12803  algcvg  12804  algcvga  12807  algfx  12808  eucalglt  12813  lcmid  12836  qredeu  12853  prmfac1  12908  sqne2sq  12933  qnumdenbi  12948  dfphi2  12976  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  phisum  12997  pcmpt  13100  pcfac  13107  1arithlem4  13123  elgz  13128  4sqlem4  13149  4sqlem12  13159  2expltfac  13196  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfileme  13214  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilem4  13219  ballotfilemi  13221  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemrval  13239  ballotfilemrc  13252  ballotfilemrinv  13255  ballotfilemth  13259  ballotfi  13260  ennnfonelemk  13269  ennnfonelemp1  13275  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemrn  13288  ennnfonelemnn0  13291  ennnfonelemr  13292  ennnfonelemim  13293  ctinfomlemom  13296  ctinfom  13297  ctiunctlemfo  13308  nninfdclemlt  13320  nninfdclemf1  13321  sloteq  13335  ressvalsets  13395  topnvalg  13582  imasex  13603  imasaddvallemg  13613  qusex  13623  xpsfrnel  13642  xpsfeq  13643  ismgm  13654  plusffvalg  13659  grpidvalg  13670  gzsumfzval  13688  gzsumval2  13691  issgrp  13695  ismnddef  13708  ismhm  13745  mhmex  13746  mhmlin  13751  issubm  13756  mhmeql  13776  isgrp  13788  grpn0  13817  grpinvfvalg  13824  grpsubfvalg  13827  grpsubval  13828  grpinv11  13851  grpinvnz  13853  mhmlem  13894  mulgfvalg  13901  mulgsubcl  13916  mulgaddcomlem  13925  mulgneg2  13936  mulgass  13939  issubg  13953  subgex  13956  issubg2m  13969  issubg4m  13973  0subg  13979  isnsg  13982  releqgg  14000  eqgex  14001  eqgval  14003  isghm  14023  ghmlin  14028  ghmrn  14037  ghmeql  14047  f1ghm0to0  14052  iscmn  14073  gsumconstcmn  14143  prdsbasprj  14159  prdsplusgfval  14161  prdsmulrfval  14163  prdsidlem  14170  prdsinvlem  14173  xpsval  14178  pws0g  14190  pwsinvg  14192  pwssub  14193  mgpvalg  14197  isrng  14208  issrg  14243  srgfcl  14251  isring  14278  iscrng  14281  mulgass2  14336  opprvalg  14347  dvdsrvald  14373  isunitd  14386  invrfvald  14402  dvrfvald  14413  dvrvald  14414  isrhm  14438  rhmval  14453  isnzr  14461  islring  14472  issubrng  14480  issubrg  14502  rrgval  14543  rrgsupp  14547  isdomn  14551  aprval  14564  aprap  14571  aprprop  14574  isdrngtap  14579  islmod  14600  scaffvalg  14615  lsssetm  14665  lspfval  14697  sraval  14746  rlmvalg  14763  2idlval  14811  2idlvalg  14812  cnfldmulg  14885  zlmval  14934  znf1o  14958  psrlinv  14998  mplsubgfilemcl  15013  istps  15056  clsfval  15125  cnpval  15222  lmconst  15240  txcnp  15295  upxp  15296  uptx  15298  txlm  15303  lmcn2  15304  cnmpt11  15307  cnmpt11f  15308  cnmpt1t  15309  cnmpt21  15315  cnmpt21f  15316  cnmpt2t  15317  mopnval  15466  isxms  15475  isms  15477  comet  15523  mopnex  15529  xmetxp  15531  xmetxpbl  15532  txmetcnp  15542  txmetcn  15543  qtopbasss  15545  cncfi  15602  cncfmpt1f  15622  ivthinclemlm  15658  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthdec  15668  ivthreinc  15669  cnlimci  15697  limccnpcntop  15699  eldvap  15706  dvcoapbr  15731  dvcj  15733  dvfre  15734  dvmptcjx  15748  dveflem  15750  elply2  15759  elplyd  15765  plymullem1  15772  plyadd  15775  plymul  15776  plycoeid3  15781  plycolemc  15782  plyco  15783  plycjlemc  15784  plycj  15785  dvply1  15789  sin0pilem2  15806  pilem3  15807  coseq0q4123  15858  coseq0negpitopi  15860  cos11  15877  logltb  15898  logfac  15918  rpcxpef  15919  rplogbval  15970  pellexlem1  16005  pellexlem3  16007  mpodvdsmulf1o  16018  fsumdvdsmul  16019  zabsle1  16032  lgslem2  16034  lgslem3  16035  lgsfcl2  16039  lgsfle1  16042  lgsle1  16048  lgsdirprm  16067  lgseisenlem2  16104  lgsquadlem2  16111  2sqlem1  16147  2sqlem2  16148  mul2sq  16149  2sqlem3  16150  2sqlem9  16157  2sqlem10  16158  vtxvalg  16171  iedgvalg  16172  edgvalg  16214  edgopval  16217  edgstruct  16219  isuhgrm  16226  isushgrm  16227  isupgren  16250  isumgren  16260  isuspgren  16312  isusgren  16313  umgr2edg1  16364  usgredg2vlem1  16377  usgredg2vlem2  16378  ushgredgedg  16381  issubgr  16412  vtxdgfval  16443  vtxedgfi  16444  vtxdg0v  16449  vtxdumgrfival  16453  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  wkslem1  16475  wkslem2  16476  wksfval  16477  iswlk  16478  uspgr2wlkeq  16520  uspgr2wlkeqi  16522  2wlklem  16531  trlsfvalg  16538  clwwlkg  16548  isclwwlk  16549  clwwlkccatlem  16555  clwwlkng  16560  clwwlkn2  16576  clwwlkext2edg  16577  umgr2cwwk2dif  16579  umgr2cwwkdifex  16580  clwwlknonmpo  16583  clwwlknonel  16587  clwwlknonex2lem2  16593  eupthsg  16600  iseupth  16602  eupthseg  16607  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lem3fi  16631  eupth2lemsfi  16633  eupth2fi  16634  eulerpathprum  16635  konigsberglem4  16646  depindlem1  16661  depindlem2  16662  depindlem3  16663  012of  16937  2o01f  16938  subctctexmid  16944  nnsf  16953  nninfalllem1  16956  nninffeq  16968  qdencn  16977  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trilpo  16997  iswomni0  17006  redcwlpo  17010  dceqnconst  17015  dcapnconst  17016  nconstwlpolemgt0  17019  nconstwlpolem  17020  nconstwlpo  17021  neapmkv  17023