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  10854  frec2uzltd  10855  frec2uzlt2d  10856  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgtcl  10864  frecuzrdgg  10868  frecuzrdgfunlem  10871  frecfzennn  10878  seqeq1  10902  iseqovex  10910  seq3val  10912  seqvalcd  10913  seq3-1  10914  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3clss  10923  seq3fveq2  10927  seqfveq2g  10929  seqfveqg  10930  seq3fveq  10931  seq3feq  10932  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  ser3mono  10939  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqval  10952  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1olemp  10967  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem2a  10970  seqf1og  10973  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  ser3le  10989  exp3vallem  10992  exp3val  10993  facp1  11184  faccl  11189  facdiv  11192  facwordi  11194  faclbnd  11195  facubnd  11199  bcval  11203  bcval5  11217  fz1eqb  11245  omgadd  11258  hashxp  11283  hashmap  11284  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  hashf1  11303  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  eqwrd  11361  lswwrd  11367  lswex  11372  ccatfvalfi  11376  ccatval1  11381  ccatval2  11382  ccatalpha  11397  s1eq  11403  eqs1  11412  swrdval  11436  ccatopth2  11505  wrd2ind  11511  seq3shft  11619  reval  11630  replim  11640  cj11  11687  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  rexuz3  11772  absval  11783  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  resqrexlemsqa  11806  resqrexlemex  11807  abs00bd  11848  cau3lem  11897  caubnd2  11900  fiidxsupcl  12012  climconst  12075  climmpt  12085  climshftlemg  12087  climcn1  12093  climle  12119  climub  12129  climserle  12130  climcau  12132  climcvg1nlem  12134  climcvg1n  12135  serf0  12137  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  summodclem2  12168  summodc  12169  zsumdc  12170  fsum3  12173  fsumf1o  12176  fisumss  12178  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumadd  12192  sumsnf  12195  isummulc2  12212  isumge0  12216  isumadd  12217  fsum2dlemstep  12220  fsummulc2  12234  fsumconst  12240  fsumrelem  12257  isumshft  12276  isum1p  12278  isumnn0nn  12279  isumrpcl  12280  isumlessdc  12282  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2prod  12325  prodfap0  12331  prodfrecap  12332  prodfdivap  12333  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodf1o  12374  fprodssdc  12376  fprodmul  12377  prodsnf  12378  fprodfac  12401  fprodconst  12406  fprod2dlemstep  12408  eftvalcn  12443  ef0lem  12446  ege2le3  12457  efcj  12459  efaddlem  12460  eftlub  12476  efgt1p2  12481  reef11  12485  tanvalap  12494  efieq1re  12558  eirraplem  12563  dvdsabseq  12633  dvdsfac  12646  gcd0id  12775  nninfctlemfo  12836  nn0seqcvgd  12838  alginv  12844  algcvg  12845  algcvga  12848  algfx  12849  eucalglt  12854  lcmid  12877  qredeu  12894  prmfac1  12950  sqne2sq  12976  qnumdenbi  12991  dfphi2  13021  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  phisum  13042  pcmpt  13145  pcfac  13152  1arithlem4  13168  elgz  13173  4sqlem4  13194  4sqlem12  13204  2expltfac  13242  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfileme  13288  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  ballotfilemi  13295  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemrval  13313  ballotfilemrc  13326  ballotfilemrinv  13329  ballotfilemth  13333  ballotfi  13334  ennnfonelemk  13343  ennnfonelemp1  13349  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemrn  13362  ennnfonelemnn0  13365  ennnfonelemr  13366  ennnfonelemim  13367  ctinfomlemom  13370  ctinfom  13371  ctiunctlemfo  13382  nninfdclemlt  13394  nninfdclemf1  13395  sloteq  13409  ressvalsets  13470  topnvalg  13658  imasex  13679  imasaddvallemg  13689  qusex  13699  xpsfrnel  13718  xpsfeq  13719  ismgm  13730  plusffvalg  13735  grpidvalg  13746  gzsumfzval  13764  gzsumval2  13767  issgrp  13771  ismnddef  13784  ismhm  13821  mhmex  13822  mhmlin  13827  issubm  13832  mhmeql  13852  isgrp  13864  grpn0  13893  grpinvfvalg  13900  grpsubfvalg  13903  grpsubval  13904  grpinv11  13927  grpinvnz  13929  mhmlem  13970  mulgfvalg  13977  mulgsubcl  13992  mulgaddcomlem  14001  mulgneg2  14012  mulgass  14015  issubg  14029  subgex  14032  issubg2m  14045  issubg4m  14049  0subg  14055  isnsg  14058  releqgg  14076  eqgex  14077  eqgval  14079  isghm  14099  ghmlin  14104  ghmrn  14113  ghmeql  14123  f1ghm0to0  14128  cntzex  14144  cntrval  14145  cntzfval  14146  iscmn  14180  gsumconstcmn  14250  prdsbasprj  14266  prdsplusgfval  14268  prdsmulrfval  14270  prdsidlem  14277  prdsinvlem  14280  xpsval  14285  pws0g  14297  pwsinvg  14299  pwssub  14300  mgpvalg  14304  isrng  14317  issrg  14353  srgfcl  14361  isring  14388  iscrng  14391  mulgass2  14447  opprvalg  14458  dvdsrvald  14484  isunitd  14497  invrfvald  14513  dvrfvald  14524  dvrvald  14525  isrhm  14549  rhmval  14564  isnzr  14572  islring  14583  issubrng  14591  issubrg  14613  rrgval  14654  rrgsupp  14658  isdomn  14662  aprval  14675  aprap  14682  aprprop  14685  isdrngtap  14690  islmod  14711  scaffvalg  14727  lsssetm  14777  lspfval  14809  sraval  14858  rlmvalg  14875  2idlval  14923  2idlvalg  14924  cnfldmulg  14997  zlmval  15046  znf1o  15070  isassa  15086  aspval  15099  asclfval  15105  psrbaglefifi  15147  psrlinv  15166  mplsubgfilemcl  15181  istps  15224  clsfval  15293  cnpval  15390  lmconst  15408  txcnp  15463  upxp  15464  uptx  15466  txlm  15471  lmcn2  15472  cnmpt11  15475  cnmpt11f  15476  cnmpt1t  15477  cnmpt21  15483  cnmpt21f  15484  cnmpt2t  15485  mopnval  15634  isxms  15643  isms  15645  comet  15691  mopnex  15697  xmetxp  15699  xmetxpbl  15700  txmetcnp  15710  txmetcn  15711  qtopbasss  15713  cncfi  15770  cncfmpt1f  15790  ivthinclemlm  15826  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthdec  15836  ivthreinc  15837  cnlimci  15865  limccnpcntop  15867  eldvap  15874  dvcoapbr  15899  dvcj  15901  dvfre  15902  dvmptcjx  15916  dveflem  15918  elply2  15927  elplyd  15933  plymullem1  15940  plyadd  15943  plymul  15944  plycoeid3  15949  plycolemc  15950  plyco  15951  plycjlemc  15952  plycj  15953  dvply1  15957  sin0pilem2  15975  pilem3  15976  coseq0q4123  16027  coseq0negpitopi  16029  cos11  16046  logltb  16068  logfac  16090  rpcxpef  16091  rplogbval  16142  pellexlem1  16190  pellexlem3  16192  efnnfsumcl  16200  chtprm  16222  efchtqdvds  16226  ppiqltx  16242  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  chtqub  16257  bposlem5  16276  bposlem7  16278  bposlem8  16279  bposlem9  16280  zabsle1  16284  lgslem2  16286  lgslem3  16287  lgsfcl2  16291  lgsfle1  16294  lgsle1  16300  lgsdirprm  16319  lgseisenlem2  16356  lgsquadlem2  16363  2sqlem1  16399  2sqlem2  16400  mul2sq  16401  2sqlem3  16402  2sqlem9  16409  2sqlem10  16410  vtxvalg  16423  iedgvalg  16424  edgvalg  16466  edgopval  16469  edgstruct  16471  isuhgrm  16478  isushgrm  16479  isupgren  16502  isumgren  16512  isuspgren  16564  isusgren  16565  umgr2edg1  16616  usgredg2vlem1  16629  usgredg2vlem2  16630  ushgredgedg  16633  issubgr  16664  vtxdgfval  16695  vtxedgfi  16696  vtxdg0v  16701  vtxdumgrfival  16705  1loopgrvd0fi  16713  1hevtxdg0fi  16714  1hevtxdg1en  16715  wkslem1  16727  wkslem2  16728  wksfval  16729  iswlk  16730  uspgr2wlkeq  16772  uspgr2wlkeqi  16774  2wlklem  16783  trlsfvalg  16790  clwwlkg  16800  isclwwlk  16801  clwwlkccatlem  16807  clwwlkng  16812  clwwlkn2  16828  clwwlkext2edg  16829  umgr2cwwk2dif  16831  umgr2cwwkdifex  16832  clwwlknonmpo  16835  clwwlknonel  16839  clwwlknonex2lem2  16845  eupthsg  16852  iseupth  16854  eupthseg  16859  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lem3fi  16883  eupth2lemsfi  16885  eupth2fi  16886  eulerpathprum  16887  konigsberglem4  16898  depindlem1  16913  depindlem2  16914  depindlem3  16915  012of  17189  2o01f  17190  subctctexmid  17196  nnsf  17214  nninfalllem1  17217  nninffeq  17229  qdencn  17238  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trilpo  17259  iswomni0  17268  redcwlpo  17272  dceqnconst  17277  dcapnconst  17278  nconstwlpolemgt0  17281  nconstwlpolem  17282  nconstwlpo  17283  neapmkv  17285