Theorem fveq2 5516

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 4007	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5200	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5225	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5225	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2235	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4004   iotacio 5177   ` cfv 5217

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  fveq2i  5519  fveq2d  5520  2fveq3  5521  fvifdc  5538  dffn5imf  5572  fvelimab  5573  ssimaex  5578  fvco4  5589  fvmptssdm  5601  fvmptf  5609  eqfnfv2f  5618  fvelrn  5648  ralrnmpt  5659  rexrnmpt  5660  ffnfvf  5676  fmptco  5683  cofmpt  5686  fcompt  5687  fcoconst  5688  fnressn  5703  fressnfv  5704  fconstfvm  5735  foco2  5755  funiunfvdmf  5765  f1veqaeq  5770  dff13f  5771  f1fveq  5773  f1elima  5774  f1ocnvfv  5780  f1ocnvfvb  5781  fcofo  5785  cocan2  5789  fliftfun  5797  isorel  5809  isocnv  5812  isotr  5817  f1oiso2  5828  canth  5829  imbrov2fvoveq  5900  ffnov  5979  eqfnov  5981  fnovim  5983  fnrnov  6020  foov  6021  funimassov  6024  ovelimab  6025  suppssfv  6079  ofvalg  6092  ofrval  6093  offval2  6098  ofrfval2  6099  ofco  6101  caofinvl  6105  op1std  6149  op2ndd  6150  1stval2  6156  2ndval2  6157  unielxp  6175  reldm  6187  oprabco  6218  2ndconst  6223  f1o2ndf1  6229  mpoxopn0yelv  6240  mpoxopoveq  6241  smoel  6301  tfrlem1  6309  tfrlem3-2d  6313  tfrlem5  6315  tfrlem9  6320  tfr0dm  6323  tfrlemiubacc  6331  tfrlemi1  6333  tfrexlem  6335  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemubacc  6347  tfr1onlemaccex  6349  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemubacc  6360  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  tfrcl  6365  tfri3  6368  rdgtfr  6375  rdgss  6384  rdgisuc1  6385  rdgisucinc  6386  rdgon  6387  frecabex  6399  frecabcl  6400  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  frecrdg  6409  oav  6455  omv  6456  oeiv  6457  fvixp  6703  cbvixp  6715  mptelixpg  6734  elixpsn  6735  dom2lem  6772  xpcomco  6826  xpmapen  6850  fidceq  6869  fieq0  6975  ordiso2  7034  djune  7077  updjudhcoinlf  7079  updjudhcoinrg  7080  updjud  7081  omp1eom  7094  0ct  7106  ctmlemr  7107  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  nnnninfeq  7126  nnnninfeq2  7127  enomnilem  7136  finomni  7138  fodjuomnilemdc  7142  fodju0  7145  fodjuomni  7147  ismkvnex  7153  fodjumkv  7158  nninfwlporlemd  7170  nninfwlpor  7172  exmidaclem  7207  cc1  7264  cc2lem  7265  cc2  7266  cc3  7267  mulpipq2  7370  genipv  7508  genpelxp  7510  addcanprleml  7613  addcanprlemu  7614  recexprlemm  7623  recexprlemdisj  7629  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  cauappcvgprlemm  7644  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlem2  7659  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgsrlemcl  7788  caucvgsrlemfv  7790  caucvgsrlembound  7793  caucvgsrlemgt1  7794  caucvgsrlemoffval  7795  caucvgsrlemoffres  7799  caucvgsrlembnd  7800  caucvgsr  7801  axcaucvglemcau  7897  axcaucvglemres  7898  uz11  9550  cnref1o  9650  fzprval  10082  fztpval  10083  frec2uzuzd  10402  frec2uzltd  10403  frec2uzlt2d  10404  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgtcl  10412  frecuzrdgg  10416  frecuzrdgfunlem  10419  frecfzennn  10426  seqeq1  10448  iseqovex  10456  seq3val  10458  seqvalcd  10459  seq3-1  10460  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3clss  10467  seq3fveq2  10469  seq3fveq  10471  seq3feq  10472  seq3shft2  10473  monoord  10476  monoord2  10477  ser3mono  10478  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemkle  10484  iseqf1olemklt  10485  iseqf1olemqval  10487  iseqf1olemqk  10494  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1olemp  10502  seq3f1oleml  10503  seq3f1o  10504  seq3id2  10509  seq3homo  10510  seq3z  10511  ser3ge0  10517  ser3le  10518  exp3vallem  10521  exp3val  10522  facp1  10710  faccl  10715  facdiv  10718  facwordi  10720  faclbnd  10721  facubnd  10725  bcval  10729  bcval5  10743  fz1eqb  10770  omgadd  10782  hashxp  10806  zfz1isolem1  10820  zfz1iso  10821  seq3coll  10822  seq3shft  10847  reval  10858  replim  10868  cj11  10914  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  rexuz3  10999  absval  11010  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemga  11032  resqrexlemsqa  11033  resqrexlemex  11034  abs00bd  11075  cau3lem  11123  caubnd2  11126  climconst  11298  climmpt  11308  climshftlemg  11310  climcn1  11316  climle  11342  climub  11352  climserle  11353  climcau  11355  climcvg1nlem  11357  climcvg1n  11358  serf0  11360  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3  11395  fsumf1o  11398  fisumss  11400  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumadd  11414  sumsnf  11417  isummulc2  11434  isumge0  11438  isumadd  11439  fsum2dlemstep  11442  fsummulc2  11456  fsumconst  11462  fsumrelem  11479  isumshft  11498  isum1p  11500  isumnn0nn  11501  isumrpcl  11502  isumlessdc  11504  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemseq  11534  cvgratnnlemabsle  11535  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2prod  11547  prodfap0  11553  prodfrecap  11554  prodfdivap  11555  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodf1o  11596  fprodssdc  11598  fprodmul  11599  prodsnf  11600  fprodfac  11623  fprodconst  11628  fprod2dlemstep  11630  eftvalcn  11665  ef0lem  11668  ege2le3  11679  efcj  11681  efaddlem  11682  eftlub  11698  efgt1p2  11703  reef11  11707  tanvalap  11716  efieq1re  11779  eirraplem  11784  dvdsabseq  11853  dvdsfac  11866  zsupcllemex  11947  infssuzex  11950  suprzubdc  11953  gcd0id  11980  nn0seqcvgd  12041  alginv  12047  algcvg  12048  algcvga  12051  algfx  12052  eucalglt  12057  lcmid  12080  qredeu  12097  prmfac1  12152  sqne2sq  12177  qnumdenbi  12192  dfphi2  12220  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  phisum  12240  pcmpt  12341  pcfac  12348  1arithlem4  12364  elgz  12369  4sqlem4  12390  ennnfonelemk  12401  ennnfonelemp1  12407  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemrn  12420  ennnfonelemnn0  12423  ennnfonelemr  12424  ennnfonelemim  12425  ctinfomlemom  12428  ctinfom  12429  ctiunctlemfo  12440  nninfdclemlt  12452  nninfdclemf1  12453  sloteq  12467  ressvalsets  12524  topnvalg  12700  imasex  12726  imasaddvallemg  12736  xpsfrnel  12763  xpsfeq  12764  xpsval  12771  ismgm  12776  plusffvalg  12781  grpidvalg  12792  issgrp  12809  ismnddef  12819  ismhm  12853  mhmlin  12858  issubm  12863  mhmeql  12876  isgrp  12883  grpn0  12908  grpinvfvalg  12915  grpsubfvalg  12918  grpsubval  12919  grpinv11  12939  grpinvnz  12941  mhmlem  12978  mulgfvalg  12985  mulgsubcl  12997  mulgaddcomlem  13006  mulgneg2  13017  mulgass  13020  issubg  13033  subgex  13036  issubg2m  13049  issubg4m  13053  0subg  13059  isnsg  13062  releqgg  13080  eqgval  13082  iscmn  13096  mgpvalg  13133  issrg  13148  srgfcl  13156  isring  13183  iscrng  13186  mulgass2  13235  opprvalg  13241  reldvdsrsrg  13261  dvdsrvald  13262  isunitd  13275  invrfvald  13291  dvrfvald  13302  dvrvald  13303  isnzr  13325  islring  13333  issubrg  13342  aprval  13372  aprap  13376  islmod  13381  scaffvalg  13396  cnfldmulg  13473  istps  13535  clsfval  13604  cnpval  13701  lmconst  13719  txcnp  13774  upxp  13775  uptx  13777  txlm  13782  lmcn2  13783  cnmpt11  13786  cnmpt11f  13787  cnmpt1t  13788  cnmpt21  13794  cnmpt21f  13795  cnmpt2t  13796  mopnval  13945  isxms  13954  isms  13956  comet  14002  mopnex  14008  xmetxp  14010  xmetxpbl  14011  txmetcnp  14021  txmetcn  14022  qtopbasss  14024  cncfi  14068  cncfmpt1f  14087  ivthinclemlm  14115  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemdisj  14121  ivthinclemloc  14122  ivthinc  14124  ivthdec  14125  cnlimci  14145  limccnpcntop  14147  eldvap  14154  dvcoapbr  14174  dvcj  14176  dvfre  14177  dvmptcjx  14189  dveflem  14190  sin0pilem2  14206  pilem3  14207  coseq0q4123  14258  coseq0negpitopi  14260  cos11  14277  logltb  14298  rpcxpef  14318  rplogbval  14366  zabsle1  14403  lgslem2  14405  lgslem3  14406  lgsfcl2  14410  lgsfle1  14413  lgsle1  14419  lgsdirprm  14438  lgseisenlem2  14454  2sqlem1  14464  2sqlem2  14465  mul2sq  14466  2sqlem3  14467  2sqlem9  14474  2sqlem10  14475  012of  14748  2o01f  14749  subctctexmid  14753  nnsf  14757  nninfalllem1  14760  nninffeq  14772  qdencn  14778  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trilpo  14794  iswomni0  14802  redcwlpo  14806  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814  nconstwlpolem  14815  nconstwlpo  14816  neapmkv  14818