Theorem fveq2 5561

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 4037	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5242	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5267	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5267	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034  ℩cio 5218  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq2i  5564  fveq2d  5565  2fveq3  5566  fvifdc  5583  dffn5imf  5619  fvelimab  5620  ssimaex  5625  fvco4  5636  fvmptssdm  5649  fvmptf  5657  eqfnfv2f  5666  fvelrn  5696  ralrnmpt  5707  rexrnmpt  5708  ffnfvf  5724  fmptco  5731  cofmpt  5734  fcompt  5735  fcoconst  5736  fnressn  5751  fressnfv  5752  fconstfvm  5783  foco2  5803  funiunfvdmf  5814  f1veqaeq  5819  dff13f  5820  f1fveq  5822  f1elima  5823  f1ocnvfv  5829  f1ocnvfvb  5830  fcofo  5834  cocan2  5838  fliftfun  5846  isorel  5858  isocnv  5861  isotr  5866  f1oiso2  5877  canth  5878  imbrov2fvoveq  5950  ffnov  6030  eqfnov  6033  fnovim  6035  fnrnov  6073  foov  6074  funimassov  6077  ovelimab  6078  suppssfv  6135  ofvalg  6149  ofrval  6150  offval2  6155  ofrfval2  6156  ofco  6158  caofinvl  6165  op1std  6215  op2ndd  6216  1stval2  6222  2ndval2  6223  unielxp  6241  reldm  6253  oprabco  6284  2ndconst  6289  f1o2ndf1  6295  mpoxopn0yelv  6306  mpoxopoveq  6307  smoel  6367  tfrlem1  6375  tfrlem3-2d  6379  tfrlem5  6381  tfrlem9  6386  tfr0dm  6389  tfrlemiubacc  6397  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  tfrcl  6431  tfri3  6434  rdgtfr  6441  rdgss  6450  rdgisuc1  6451  rdgisucinc  6452  rdgon  6453  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  frecrdg  6475  oav  6521  omv  6522  oeiv  6523  fvixp  6771  cbvixp  6783  mptelixpg  6802  elixpsn  6803  dom2lem  6840  xpcomco  6894  xpmapen  6920  fidceq  6939  fieq0  7051  ordiso2  7110  djune  7153  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eom  7170  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  fodjuomnilemdc  7219  fodju0  7222  fodjuomni  7224  ismkvnex  7230  fodjumkv  7235  nninfwlporlemd  7247  nninfwlpor  7249  exmidaclem  7293  cc1  7350  cc2lem  7351  cc2  7352  cc3  7353  mulpipq2  7457  genipv  7595  genpelxp  7597  addcanprleml  7700  addcanprlemu  7701  recexprlemm  7710  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  cauappcvgprlemm  7731  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnkeqj  7776  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  caucvgprprlem1  7795  caucvgprprlem2  7796  caucvgsrlemcl  7875  caucvgsrlemfv  7877  caucvgsrlembound  7880  caucvgsrlemgt1  7881  caucvgsrlemoffval  7882  caucvgsrlemoffres  7886  caucvgsrlembnd  7887  caucvgsr  7888  axcaucvglemcau  7984  axcaucvglemres  7985  uz11  9643  cnref1o  9744  fzprval  10176  fztpval  10177  zsupcllemex  10339  infssuzex  10342  suprzubdc  10345  frec2uzuzd  10513  frec2uzltd  10514  frec2uzlt2d  10515  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgtcl  10523  frecuzrdgg  10527  frecuzrdgfunlem  10530  frecfzennn  10537  seqeq1  10561  iseqovex  10569  seq3val  10571  seqvalcd  10572  seq3-1  10573  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3clss  10582  seq3fveq2  10586  seqfveq2g  10588  seqfveqg  10589  seq3fveq  10590  seq3feq  10591  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqval  10611  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1olemp  10626  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem2a  10629  seqf1og  10632  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  ser3le  10648  exp3vallem  10651  exp3val  10652  facp1  10841  faccl  10846  facdiv  10849  facwordi  10851  faclbnd  10852  facubnd  10856  bcval  10860  bcval5  10874  fz1eqb  10901  omgadd  10913  hashxp  10937  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  eqwrd  10994  seq3shft  11022  reval  11033  replim  11043  cj11  11089  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  rexuz3  11174  absval  11185  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  resqrexlemsqa  11208  resqrexlemex  11209  abs00bd  11250  cau3lem  11298  caubnd2  11301  climconst  11474  climmpt  11484  climshftlemg  11486  climcn1  11492  climle  11518  climub  11528  climserle  11529  climcau  11531  climcvg1nlem  11533  climcvg1n  11534  serf0  11536  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  fsumf1o  11574  fisumss  11576  fsum3cvg2  11578  fsum3ser  11581  fsumcl2lem  11582  fsumadd  11590  sumsnf  11593  isummulc2  11610  isumge0  11614  isumadd  11615  fsum2dlemstep  11618  fsummulc2  11632  fsumconst  11638  fsumrelem  11655  isumshft  11674  isum1p  11676  isumnn0nn  11677  isumrpcl  11678  isumlessdc  11680  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemseq  11710  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  clim2prod  11723  prodfap0  11729  prodfrecap  11730  prodfdivap  11731  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  prodsnf  11776  fprodfac  11799  fprodconst  11804  fprod2dlemstep  11806  eftvalcn  11841  ef0lem  11844  ege2le3  11855  efcj  11857  efaddlem  11858  eftlub  11874  efgt1p2  11879  reef11  11883  tanvalap  11892  efieq1re  11956  eirraplem  11961  dvdsabseq  12031  dvdsfac  12044  gcd0id  12173  nninfctlemfo  12234  nn0seqcvgd  12236  alginv  12242  algcvg  12243  algcvga  12246  algfx  12247  eucalglt  12252  lcmid  12275  qredeu  12292  prmfac1  12347  sqne2sq  12372  qnumdenbi  12387  dfphi2  12415  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  phisum  12436  pcmpt  12539  pcfac  12546  1arithlem4  12562  elgz  12567  4sqlem4  12588  4sqlem12  12598  2expltfac  12635  ennnfonelemk  12644  ennnfonelemp1  12650  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrn  12663  ennnfonelemnn0  12666  ennnfonelemr  12667  ennnfonelemim  12668  ctinfomlemom  12671  ctinfom  12672  ctiunctlemfo  12683  nninfdclemlt  12695  nninfdclemf1  12696  sloteq  12710  ressvalsets  12769  topnvalg  12955  prdsbasprj  12986  prdsplusgfval  12988  prdsmulrfval  12990  imasex  13009  imasaddvallemg  13019  qusex  13029  xpsfrnel  13048  xpsfeq  13049  xpsval  13056  ismgm  13061  plusffvalg  13066  grpidvalg  13077  gsumfzval  13095  gsumval2  13101  issgrp  13107  ismnddef  13122  prdsidlem  13151  pws0g  13155  ismhm  13165  mhmex  13166  mhmlin  13171  issubm  13176  mhmeql  13196  isgrp  13210  grpn0  13239  grpinvfvalg  13246  grpsubfvalg  13249  grpsubval  13250  grpinv11  13273  grpinvnz  13275  prdsinvlem  13312  pwsinvg  13316  pwssub  13317  mhmlem  13322  mulgfvalg  13329  mulgsubcl  13344  mulgaddcomlem  13353  mulgneg2  13364  mulgass  13367  issubg  13381  subgex  13384  issubg2m  13397  issubg4m  13401  0subg  13407  isnsg  13410  releqgg  13428  eqgex  13429  eqgval  13431  isghm  13451  ghmlin  13456  ghmrn  13465  ghmeql  13475  f1ghm0to0  13480  iscmn  13501  mgpvalg  13557  isrng  13568  issrg  13599  srgfcl  13607  isring  13634  iscrng  13637  mulgass2  13692  opprvalg  13703  reldvdsrsrg  13726  dvdsrvald  13727  isunitd  13740  invrfvald  13756  dvrfvald  13767  dvrvald  13768  isrhm  13792  rhmval  13807  isnzr  13815  islring  13826  issubrng  13833  issubrg  13855  rrgval  13896  isdomn  13903  aprval  13916  aprap  13920  islmod  13925  scaffvalg  13940  lsssetm  13990  lspfval  14022  sraval  14071  rlmvalg  14088  2idlval  14136  2idlvalg  14137  cnfldmulg  14210  zlmval  14261  znf1o  14285  psrlinv  14318  mplsubgfilemcl  14333  istps  14376  clsfval  14445  cnpval  14542  lmconst  14560  txcnp  14615  upxp  14616  uptx  14618  txlm  14623  lmcn2  14624  cnmpt11  14627  cnmpt11f  14628  cnmpt1t  14629  cnmpt21  14635  cnmpt21f  14636  cnmpt2t  14637  mopnval  14786  isxms  14795  isms  14797  comet  14843  mopnex  14849  xmetxp  14851  xmetxpbl  14852  txmetcnp  14862  txmetcn  14863  qtopbasss  14865  cncfi  14922  cncfmpt1f  14942  ivthinclemlm  14978  ivthinclemum  14979  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  ivthinc  14987  ivthdec  14988  ivthreinc  14989  cnlimci  15017  limccnpcntop  15019  eldvap  15026  dvcoapbr  15051  dvcj  15053  dvfre  15054  dvmptcjx  15068  dveflem  15070  elply2  15079  elplyd  15085  plymullem1  15092  plyadd  15095  plymul  15096  plycoeid3  15101  plycolemc  15102  plyco  15103  plycjlemc  15104  plycj  15105  dvply1  15109  sin0pilem2  15126  pilem3  15127  coseq0q4123  15178  coseq0negpitopi  15180  cos11  15197  logltb  15218  rpcxpef  15238  rplogbval  15289  mpodvdsmulf1o  15334  fsumdvdsmul  15335  zabsle1  15348  lgslem2  15350  lgslem3  15351  lgsfcl2  15355  lgsfle1  15358  lgsle1  15364  lgsdirprm  15383  lgseisenlem2  15420  lgsquadlem2  15427  2sqlem1  15463  2sqlem2  15464  mul2sq  15465  2sqlem3  15466  2sqlem9  15473  2sqlem10  15474  012of  15748  2o01f  15749  subctctexmid  15755  nnsf  15760  nninfalllem1  15763  nninffeq  15775  qdencn  15784  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trilpo  15800  iswomni0  15808  redcwlpo  15812  dceqnconst  15817  dcapnconst  15818  nconstwlpolemgt0  15821  nconstwlpolem  15822  nconstwlpo  15823  neapmkv  15825