Theorem fveq2 5555

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

Assertion

Ref	Expression
fveq2	|- ( A = B -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 4033	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5238	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5263	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5263	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2251	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4030   iotacio 5214   ` cfv 5255

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  fveq2i  5558  fveq2d  5559  2fveq3  5560  fvifdc  5577  dffn5imf  5613  fvelimab  5614  ssimaex  5619  fvco4  5630  fvmptssdm  5643  fvmptf  5651  eqfnfv2f  5660  fvelrn  5690  ralrnmpt  5701  rexrnmpt  5702  ffnfvf  5718  fmptco  5725  cofmpt  5728  fcompt  5729  fcoconst  5730  fnressn  5745  fressnfv  5746  fconstfvm  5777  foco2  5797  funiunfvdmf  5808  f1veqaeq  5813  dff13f  5814  f1fveq  5816  f1elima  5817  f1ocnvfv  5823  f1ocnvfvb  5824  fcofo  5828  cocan2  5832  fliftfun  5840  isorel  5852  isocnv  5855  isotr  5860  f1oiso2  5871  canth  5872  imbrov2fvoveq  5944  ffnov  6023  eqfnov  6026  fnovim  6028  fnrnov  6066  foov  6067  funimassov  6070  ovelimab  6071  suppssfv  6128  ofvalg  6142  ofrval  6143  offval2  6148  ofrfval2  6149  ofco  6151  caofinvl  6157  op1std  6203  op2ndd  6204  1stval2  6210  2ndval2  6211  unielxp  6229  reldm  6241  oprabco  6272  2ndconst  6277  f1o2ndf1  6283  mpoxopn0yelv  6294  mpoxopoveq  6295  smoel  6355  tfrlem1  6363  tfrlem3-2d  6367  tfrlem5  6369  tfrlem9  6374  tfr0dm  6377  tfrlemiubacc  6385  tfrlemi1  6387  tfrexlem  6389  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemubacc  6401  tfr1onlemaccex  6403  tfr1onlemres  6404  tfri1dALT  6406  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemubacc  6414  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  tfrcl  6419  tfri3  6422  rdgtfr  6429  rdgss  6438  rdgisuc1  6439  rdgisucinc  6440  rdgon  6441  frecabex  6453  frecabcl  6454  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  frecrdg  6463  oav  6509  omv  6510  oeiv  6511  fvixp  6759  cbvixp  6771  mptelixpg  6790  elixpsn  6791  dom2lem  6828  xpcomco  6882  xpmapen  6908  fidceq  6927  fieq0  7037  ordiso2  7096  djune  7139  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  omp1eom  7156  0ct  7168  ctmlemr  7169  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  finomni  7201  fodjuomnilemdc  7205  fodju0  7208  fodjuomni  7210  ismkvnex  7216  fodjumkv  7221  nninfwlporlemd  7233  nninfwlpor  7235  exmidaclem  7270  cc1  7327  cc2lem  7328  cc2  7329  cc3  7330  mulpipq2  7433  genipv  7571  genpelxp  7573  addcanprleml  7676  addcanprlemu  7677  recexprlemm  7686  recexprlemdisj  7692  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  cauappcvgprlemm  7707  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemnbj  7755  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsrlembound  7856  caucvgsrlemgt1  7857  caucvgsrlemoffval  7858  caucvgsrlemoffres  7862  caucvgsrlembnd  7863  caucvgsr  7864  axcaucvglemcau  7960  axcaucvglemres  7961  uz11  9618  cnref1o  9719  fzprval  10151  fztpval  10152  frec2uzuzd  10476  frec2uzltd  10477  frec2uzlt2d  10478  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgtcl  10486  frecuzrdgg  10490  frecuzrdgfunlem  10493  frecfzennn  10500  seqeq1  10524  iseqovex  10532  seq3val  10534  seqvalcd  10535  seq3-1  10536  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3clss  10545  seq3fveq2  10549  seqfveq2g  10551  seqfveqg  10552  seq3fveq  10553  seq3feq  10554  seq3shft2  10555  seqshft2g  10556  monoord  10559  monoord2  10560  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqval  10574  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1olemp  10589  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem2a  10592  seqf1og  10595  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  ser3le  10611  exp3vallem  10614  exp3val  10615  facp1  10804  faccl  10809  facdiv  10812  facwordi  10814  faclbnd  10815  facubnd  10819  bcval  10823  bcval5  10837  fz1eqb  10864  omgadd  10876  hashxp  10900  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  eqwrd  10957  seq3shft  10985  reval  10996  replim  11006  cj11  11052  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  rexuz3  11137  absval  11148  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc3  11163  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  resqrexlemsqa  11171  resqrexlemex  11172  abs00bd  11213  cau3lem  11261  caubnd2  11264  climconst  11436  climmpt  11446  climshftlemg  11448  climcn1  11454  climle  11480  climub  11490  climserle  11491  climcau  11493  climcvg1nlem  11495  climcvg1n  11496  serf0  11498  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  fsumf1o  11536  fisumss  11538  fsum3cvg2  11540  fsum3ser  11543  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  isummulc2  11572  isumge0  11576  isumadd  11577  fsum2dlemstep  11580  fsummulc2  11594  fsumconst  11600  fsumrelem  11617  isumshft  11636  isum1p  11638  isumnn0nn  11639  isumrpcl  11640  isumlessdc  11642  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2prod  11685  prodfap0  11691  prodfrecap  11692  prodfdivap  11693  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  prodsnf  11738  fprodfac  11761  fprodconst  11766  fprod2dlemstep  11768  eftvalcn  11803  ef0lem  11806  ege2le3  11817  efcj  11819  efaddlem  11820  eftlub  11836  efgt1p2  11841  reef11  11845  tanvalap  11854  efieq1re  11918  eirraplem  11923  dvdsabseq  11992  dvdsfac  12005  zsupcllemex  12086  infssuzex  12089  suprzubdc  12092  gcd0id  12119  nninfctlemfo  12180  nn0seqcvgd  12182  alginv  12188  algcvg  12189  algcvga  12192  algfx  12193  eucalglt  12198  lcmid  12221  qredeu  12238  prmfac1  12293  sqne2sq  12318  qnumdenbi  12333  dfphi2  12361  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  phisum  12381  pcmpt  12484  pcfac  12491  1arithlem4  12507  elgz  12512  4sqlem4  12533  4sqlem12  12543  ennnfonelemk  12560  ennnfonelemp1  12566  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemrn  12579  ennnfonelemnn0  12582  ennnfonelemr  12583  ennnfonelemim  12584  ctinfomlemom  12587  ctinfom  12588  ctiunctlemfo  12599  nninfdclemlt  12611  nninfdclemf1  12612  sloteq  12626  ressvalsets  12685  topnvalg  12865  imasex  12891  imasaddvallemg  12901  qusex  12911  xpsfrnel  12930  xpsfeq  12931  xpsval  12938  ismgm  12943  plusffvalg  12948  grpidvalg  12959  gsumfzval  12977  gsumval2  12983  issgrp  12989  ismnddef  13002  ismhm  13036  mhmex  13037  mhmlin  13042  issubm  13047  mhmeql  13067  isgrp  13081  grpn0  13110  grpinvfvalg  13117  grpsubfvalg  13120  grpsubval  13121  grpinv11  13144  grpinvnz  13146  mhmlem  13187  mulgfvalg  13194  mulgsubcl  13209  mulgaddcomlem  13218  mulgneg2  13229  mulgass  13232  issubg  13246  subgex  13249  issubg2m  13262  issubg4m  13266  0subg  13272  isnsg  13275  releqgg  13293  eqgex  13294  eqgval  13296  isghm  13316  ghmlin  13321  ghmrn  13330  ghmeql  13340  f1ghm0to0  13345  iscmn  13366  mgpvalg  13422  isrng  13433  issrg  13464  srgfcl  13472  isring  13499  iscrng  13502  mulgass2  13557  opprvalg  13568  reldvdsrsrg  13591  dvdsrvald  13592  isunitd  13605  invrfvald  13621  dvrfvald  13632  dvrvald  13633  isrhm  13657  rhmval  13672  isnzr  13680  islring  13691  issubrng  13698  issubrg  13720  rrgval  13761  isdomn  13768  aprval  13781  aprap  13785  islmod  13790  scaffvalg  13805  lsssetm  13855  lspfval  13887  sraval  13936  rlmvalg  13953  2idlval  14001  2idlvalg  14002  cnfldmulg  14075  zlmval  14126  znf1o  14150  istps  14211  clsfval  14280  cnpval  14377  lmconst  14395  txcnp  14450  upxp  14451  uptx  14453  txlm  14458  lmcn2  14459  cnmpt11  14462  cnmpt11f  14463  cnmpt1t  14464  cnmpt21  14470  cnmpt21f  14471  cnmpt2t  14472  mopnval  14621  isxms  14630  isms  14632  comet  14678  mopnex  14684  xmetxp  14686  xmetxpbl  14687  txmetcnp  14697  txmetcn  14698  qtopbasss  14700  cncfi  14757  cncfmpt1f  14777  ivthinclemlm  14813  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthdec  14823  ivthreinc  14824  cnlimci  14852  limccnpcntop  14854  eldvap  14861  dvcoapbr  14886  dvcj  14888  dvfre  14889  dvmptcjx  14903  dveflem  14905  elply2  14914  elplyd  14920  plymullem1  14927  plyadd  14930  plymul  14931  plycolemc  14936  plyco  14937  plycjlemc  14938  plycj  14939  dvply1  14943  sin0pilem2  14958  pilem3  14959  coseq0q4123  15010  coseq0negpitopi  15012  cos11  15029  logltb  15050  rpcxpef  15070  rplogbval  15118  zabsle1  15156  lgslem2  15158  lgslem3  15159  lgsfcl2  15163  lgsfle1  15166  lgsle1  15172  lgsdirprm  15191  lgseisenlem2  15228  lgsquadlem2  15235  2sqlem1  15271  2sqlem2  15272  mul2sq  15273  2sqlem3  15274  2sqlem9  15281  2sqlem10  15282  012of  15556  2o01f  15557  subctctexmid  15561  nnsf  15565  nninfalllem1  15568  nninffeq  15580  qdencn  15587  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trilpo  15603  iswomni0  15611  redcwlpo  15615  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624  nconstwlpolem  15625  nconstwlpo  15626  neapmkv  15628