Theorem fveq2 5695

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 4133	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5360	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5385	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5385	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4130   iotacio 5335   ` cfv 5377

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq2i  5698  fveq2d  5699  2fveq3  5700  fvifdc  5717  dffn5imf  5758  fvelimab  5759  ssimaex  5764  fvco4  5777  fvmptssdm  5790  fvmptf  5798  eqfnfv2f  5810  fvelrn  5839  ralrnmpt  5850  rexrnmpt  5851  ffnfvf  5867  fmptco  5874  cofmpt  5877  fcompt  5878  fcoconst  5879  fsn2g  5883  fnressn  5901  fressnfv  5902  fconstfvm  5933  dfimafnf  5955  foco2  5959  funiunfvdmf  5970  f1veqaeq  5975  dff13f  5976  f1fveq  5978  f1elima  5979  f1ocnvfv  5985  f1ocnvfvb  5986  fcofo  5990  cocan2  5994  fliftfun  6002  isorel  6014  isocnv  6017  isotr  6022  f1oiso2  6033  canth  6036  imbrov2fvoveq  6110  ffnov  6192  eqfnov  6195  fnovim  6197  fnrnov  6235  foov  6236  funimassov  6239  ovelimab  6240  ofvalg  6312  ofrval  6313  offval2  6318  ofrfval2  6319  ofco  6321  caofinvl  6328  op1std  6382  op2ndd  6383  1stval2  6389  2ndval2  6390  unielxp  6408  reldm  6420  oprabco  6453  2ndconst  6458  f1o2ndf1  6464  elsuppfng  6482  elsuppfn  6483  mpoxopn0yelv  6510  mpoxopoveq  6511  smoel  6571  tfrlem1  6579  tfrlem3-2d  6583  tfrlem5  6585  tfrlem9  6590  tfr0dm  6593  tfrlemiubacc  6601  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  tfri3  6638  rdgtfr  6645  rdgss  6654  rdgisuc1  6655  rdgisucinc  6656  rdgon  6657  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  frecrdg  6679  oav  6727  omv  6728  oeiv  6729  fvixp  6985  cbvixp  6997  mptelixpg  7016  elixpsn  7017  dom2lem  7058  xpcomco  7124  xpmapen  7150  fidceq  7171  fieq0  7310  ordiso2  7376  djune  7419  updjudhcoinlf  7421  updjudhcoinrg  7422  updjud  7423  omp1eom  7436  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  finomni  7481  fodjuomnilemdc  7485  fodju0  7488  fodjuomni  7490  ismkvnex  7496  fodjumkv  7501  nninfwlporlemd  7513  nninfwlpor  7515  exmidaclem  7565  cc1  7632  cc2lem  7633  cc2  7634  cc3  7635  mulpipq2  7739  genipv  7877  genpelxp  7879  addcanprleml  7982  addcanprlemu  7983  recexprlemm  7992  recexprlemdisj  7998  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  cauappcvgprlemm  8013  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsrlembound  8162  caucvgsrlemgt1  8163  caucvgsrlemoffval  8164  caucvgsrlemoffres  8168  caucvgsrlembnd  8169  caucvgsr  8170  axcaucvglemcau  8266  axcaucvglemres  8267  uz11  9955  cnref1o  10062  fzprval  10500  fztpval  10501  zsupcllemex  10674  infssuzex  10677  suprzubdc  10682  frec2uzuzd  10853  frec2uzltd  10854  frec2uzlt2d  10855  frecuzrdgrrn  10859  frec2uzrdg  10860  frecuzrdgtcl  10863  frecuzrdgg  10867  frecuzrdgfunlem  10870  frecfzennn  10877  seqeq1  10901  iseqovex  10909  seq3val  10911  seqvalcd  10912  seq3-1  10913  seqf  10915  seq3p1  10916  seqovcd  10918  seqp1cd  10921  seq3clss  10922  seq3fveq2  10926  seqfveq2g  10928  seqfveqg  10929  seq3fveq  10930  seq3feq  10931  seq3shft2  10932  seqshft2g  10933  monoord  10936  monoord2  10937  ser3mono  10938  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  seq3caopr2  10944  seqcaopr2g  10945  iseqf1olemkle  10948  iseqf1olemklt  10949  iseqf1olemqval  10951  iseqf1olemqk  10958  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  iseqf1olemfvp  10961  seq3f1olemqsumkj  10962  seq3f1olemqsum  10964  seq3f1olemstep  10965  seq3f1olemp  10966  seq3f1oleml  10967  seq3f1o  10968  seqf1oglem2a  10969  seqf1og  10972  seq3id2  10977  seq3homo  10978  seq3z  10979  seqhomog  10981  seqfeq4g  10982  ser3ge0  10987  ser3le  10988  exp3vallem  10991  exp3val  10992  facp1  11183  faccl  11188  facdiv  11191  facwordi  11193  faclbnd  11194  facubnd  11198  bcval  11202  bcval5  11216  fz1eqb  11244  omgadd  11257  hashxp  11282  hashmap  11283  hashfibc  11298  hashf1lem1  11300  hashf1lem2  11301  hashf1  11302  zfz1isolem1  11307  zfz1iso  11308  seq3coll  11309  eqwrd  11360  lswwrd  11366  lswex  11371  ccatfvalfi  11375  ccatval1  11380  ccatval2  11381  ccatalpha  11396  s1eq  11402  eqs1  11411  swrdval  11435  ccatopth2  11504  wrd2ind  11510  seq3shft  11618  reval  11629  replim  11639  cj11  11686  caucvgre  11762  cvg1nlemcau  11765  cvg1nlemres  11766  rexuz3  11771  absval  11782  resqrexlemover  11791  resqrexlemdecn  11793  resqrexlemlo  11794  resqrexlemcalc3  11797  resqrexlemnm  11799  resqrexlemcvg  11800  resqrexlemoverl  11802  resqrexlemglsq  11803  resqrexlemga  11804  resqrexlemsqa  11805  resqrexlemex  11806  abs00bd  11847  cau3lem  11896  caubnd2  11899  fiidxsupcl  12011  climconst  12074  climmpt  12084  climshftlemg  12086  climcn1  12092  climle  12118  climub  12128  climserle  12129  climcau  12131  climcvg1nlem  12133  climcvg1n  12134  serf0  12136  fsum3cvg  12163  summodclem3  12165  summodclem2a  12166  summodclem2  12167  summodc  12168  zsumdc  12169  fsum3  12172  fsumf1o  12175  fisumss  12177  fsum3cvg2  12179  fsum3ser  12182  fsumcl2lem  12183  fsumadd  12191  sumsnf  12194  isummulc2  12211  isumge0  12215  isumadd  12216  fsum2dlemstep  12219  fsummulc2  12233  fsumconst  12239  fsumrelem  12256  isumshft  12275  isum1p  12277  isumnn0nn  12278  isumrpcl  12279  isumlessdc  12281  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratnnlemseq  12311  cvgratnnlemabsle  12312  cvgratnnlemfm  12314  cvgratnnlemrate  12315  cvgratnn  12316  cvgratz  12317  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  clim2prod  12324  prodfap0  12330  prodfrecap  12331  prodfdivap  12332  fproddccvg  12357  prodmodclem3  12360  prodmodclem2a  12361  prodmodclem2  12362  prodmodc  12363  zproddc  12364  fprodseq  12368  fprodf1o  12373  fprodssdc  12375  fprodmul  12376  prodsnf  12377  fprodfac  12400  fprodconst  12405  fprod2dlemstep  12407  eftvalcn  12442  ef0lem  12445  ege2le3  12456  efcj  12458  efaddlem  12459  eftlub  12475  efgt1p2  12480  reef11  12484  tanvalap  12493  efieq1re  12557  eirraplem  12562  dvdsabseq  12632  dvdsfac  12645  gcd0id  12774  nninfctlemfo  12835  nn0seqcvgd  12837  alginv  12843  algcvg  12844  algcvga  12847  algfx  12848  eucalglt  12853  lcmid  12876  qredeu  12893  prmfac1  12949  sqne2sq  12975  qnumdenbi  12990  dfphi2  13020  eulerthlemrprm  13029  eulerthlema  13030  eulerthlemh  13031  eulerthlemth  13032  phisum  13041  pcmpt  13144  pcfac  13151  1arithlem4  13167  elgz  13172  4sqlem4  13193  4sqlem12  13203  2expltfac  13241  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfileme  13287  ballotfilemefi  13288  ballotfilemodife  13291  ballotfilem4  13292  ballotfilemi  13294  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemrval  13312  ballotfilemrc  13325  ballotfilemrinv  13328  ballotfilemth  13332  ballotfi  13333  ennnfonelemk  13342  ennnfonelemp1  13348  ennnfoneleminc  13353  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ennnfonelemex  13356  ennnfonelemhom  13357  ennnfonelemrn  13361  ennnfonelemnn0  13364  ennnfonelemr  13365  ennnfonelemim  13366  ctinfomlemom  13369  ctinfom  13370  ctiunctlemfo  13381  nninfdclemlt  13393  nninfdclemf1  13394  sloteq  13408  ressvalsets  13469  topnvalg  13656  imasex  13677  imasaddvallemg  13687  qusex  13697  xpsfrnel  13716  xpsfeq  13717  ismgm  13728  plusffvalg  13733  grpidvalg  13744  gzsumfzval  13762  gzsumval2  13765  issgrp  13769  ismnddef  13782  ismhm  13819  mhmex  13820  mhmlin  13825  issubm  13830  mhmeql  13850  isgrp  13862  grpn0  13891  grpinvfvalg  13898  grpsubfvalg  13901  grpsubval  13902  grpinv11  13925  grpinvnz  13927  mhmlem  13968  mulgfvalg  13975  mulgsubcl  13990  mulgaddcomlem  13999  mulgneg2  14010  mulgass  14013  issubg  14027  subgex  14030  issubg2m  14043  issubg4m  14047  0subg  14053  isnsg  14056  releqgg  14074  eqgex  14075  eqgval  14077  isghm  14097  ghmlin  14102  ghmrn  14111  ghmeql  14121  f1ghm0to0  14126  iscmn  14147  gsumconstcmn  14217  prdsbasprj  14233  prdsplusgfval  14235  prdsmulrfval  14237  prdsidlem  14244  prdsinvlem  14247  xpsval  14252  pws0g  14264  pwsinvg  14266  pwssub  14267  mgpvalg  14271  isrng  14284  issrg  14320  srgfcl  14328  isring  14355  iscrng  14358  mulgass2  14414  opprvalg  14425  dvdsrvald  14451  isunitd  14464  invrfvald  14480  dvrfvald  14491  dvrvald  14492  isrhm  14516  rhmval  14531  isnzr  14539  islring  14550  issubrng  14558  issubrg  14580  rrgval  14621  rrgsupp  14625  isdomn  14629  aprval  14642  aprap  14649  aprprop  14652  isdrngtap  14657  islmod  14678  scaffvalg  14694  lsssetm  14744  lspfval  14776  sraval  14825  rlmvalg  14842  2idlval  14890  2idlvalg  14891  cnfldmulg  14964  zlmval  15013  znf1o  15037  isassa  15053  aspval  15066  asclfval  15072  psrbaglefifi  15114  psrlinv  15127  mplsubgfilemcl  15142  istps  15185  clsfval  15254  cnpval  15351  lmconst  15369  txcnp  15424  upxp  15425  uptx  15427  txlm  15432  lmcn2  15433  cnmpt11  15436  cnmpt11f  15437  cnmpt1t  15438  cnmpt21  15444  cnmpt21f  15445  cnmpt2t  15446  mopnval  15595  isxms  15604  isms  15606  comet  15652  mopnex  15658  xmetxp  15660  xmetxpbl  15661  txmetcnp  15671  txmetcn  15672  qtopbasss  15674  cncfi  15731  cncfmpt1f  15751  ivthinclemlm  15787  ivthinclemum  15788  ivthinclemlopn  15789  ivthinclemlr  15790  ivthinclemuopn  15791  ivthinclemur  15792  ivthinclemdisj  15793  ivthinclemloc  15794  ivthinc  15796  ivthdec  15797  ivthreinc  15798  cnlimci  15826  limccnpcntop  15828  eldvap  15835  dvcoapbr  15860  dvcj  15862  dvfre  15863  dvmptcjx  15877  dveflem  15879  elply2  15888  elplyd  15894  plymullem1  15901  plyadd  15904  plymul  15905  plycoeid3  15910  plycolemc  15911  plyco  15912  plycjlemc  15913  plycj  15914  dvply1  15918  sin0pilem2  15936  pilem3  15937  coseq0q4123  15988  coseq0negpitopi  15990  cos11  16007  logltb  16029  logfac  16051  rpcxpef  16052  rplogbval  16103  pellexlem1  16151  pellexlem3  16153  efnnfsumcl  16161  chtprm  16183  efchtqdvds  16187  ppiqltx  16203  prmorcht  16204  mpodvdsmulf1o  16206  fsumdvdsmul  16207  chtqub  16218  bposlem5  16237  zabsle1  16240  lgslem2  16242  lgslem3  16243  lgsfcl2  16247  lgsfle1  16250  lgsle1  16256  lgsdirprm  16275  lgseisenlem2  16312  lgsquadlem2  16319  2sqlem1  16355  2sqlem2  16356  mul2sq  16357  2sqlem3  16358  2sqlem9  16365  2sqlem10  16366  vtxvalg  16379  iedgvalg  16380  edgvalg  16422  edgopval  16425  edgstruct  16427  isuhgrm  16434  isushgrm  16435  isupgren  16458  isumgren  16468  isuspgren  16520  isusgren  16521  umgr2edg1  16572  usgredg2vlem1  16585  usgredg2vlem2  16586  ushgredgedg  16589  issubgr  16620  vtxdgfval  16651  vtxedgfi  16652  vtxdg0v  16657  vtxdumgrfival  16661  1loopgrvd0fi  16669  1hevtxdg0fi  16670  1hevtxdg1en  16671  wkslem1  16683  wkslem2  16684  wksfval  16685  iswlk  16686  uspgr2wlkeq  16728  uspgr2wlkeqi  16730  2wlklem  16739  trlsfvalg  16746  clwwlkg  16756  isclwwlk  16757  clwwlkccatlem  16763  clwwlkng  16768  clwwlkn2  16784  clwwlkext2edg  16785  umgr2cwwk2dif  16787  umgr2cwwkdifex  16788  clwwlknonmpo  16791  clwwlknonel  16795  clwwlknonex2lem2  16801  eupthsg  16808  iseupth  16810  eupthseg  16815  eupth2lem3lem3fi  16833  eupth2lem3lem6fi  16834  eupth2lem3lem4fi  16836  eupth2lem3fi  16839  eupth2lemsfi  16841  eupth2fi  16842  eulerpathprum  16843  konigsberglem4  16854  depindlem1  16869  depindlem2  16870  depindlem3  16871  012of  17145  2o01f  17146  subctctexmid  17152  nnsf  17170  nninfalllem1  17173  nninffeq  17185  qdencn  17194  trilpolemclim  17207  trilpolemcl  17208  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  trilpo  17214  iswomni0  17223  redcwlpo  17227  dceqnconst  17232  dcapnconst  17233  nconstwlpolemgt0  17236  nconstwlpolem  17237  nconstwlpo  17238  neapmkv  17240