Theorem fveq2 5534

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 4021	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5218	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5243	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5243	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2247	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4018   iotacio 5194   ` cfv 5235

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243

This theorem is referenced by:  fveq2i  5537  fveq2d  5538  2fveq3  5539  fvifdc  5556  dffn5imf  5591  fvelimab  5592  ssimaex  5597  fvco4  5608  fvmptssdm  5620  fvmptf  5628  eqfnfv2f  5637  fvelrn  5667  ralrnmpt  5678  rexrnmpt  5679  ffnfvf  5695  fmptco  5702  cofmpt  5705  fcompt  5706  fcoconst  5707  fnressn  5722  fressnfv  5723  fconstfvm  5754  foco2  5774  funiunfvdmf  5785  f1veqaeq  5790  dff13f  5791  f1fveq  5793  f1elima  5794  f1ocnvfv  5800  f1ocnvfvb  5801  fcofo  5805  cocan2  5809  fliftfun  5817  isorel  5829  isocnv  5832  isotr  5837  f1oiso2  5848  canth  5849  imbrov2fvoveq  5920  ffnov  5999  eqfnov  6002  fnovim  6004  fnrnov  6041  foov  6042  funimassov  6045  ovelimab  6046  suppssfv  6101  ofvalg  6115  ofrval  6116  offval2  6121  ofrfval2  6122  ofco  6124  caofinvl  6128  op1std  6172  op2ndd  6173  1stval2  6179  2ndval2  6180  unielxp  6198  reldm  6210  oprabco  6241  2ndconst  6246  f1o2ndf1  6252  mpoxopn0yelv  6263  mpoxopoveq  6264  smoel  6324  tfrlem1  6332  tfrlem3-2d  6336  tfrlem5  6338  tfrlem9  6343  tfr0dm  6346  tfrlemiubacc  6354  tfrlemi1  6356  tfrexlem  6358  tfr1onlemsucfn  6364  tfr1onlemsucaccv  6365  tfr1onlembxssdm  6367  tfr1onlembfn  6368  tfr1onlemubacc  6370  tfr1onlemaccex  6372  tfr1onlemres  6373  tfri1dALT  6375  tfrcllemsucfn  6377  tfrcllemsucaccv  6378  tfrcllembxssdm  6380  tfrcllembfn  6381  tfrcllemubacc  6383  tfrcllemaccex  6385  tfrcllemres  6386  tfrcldm  6387  tfrcl  6388  tfri3  6391  rdgtfr  6398  rdgss  6407  rdgisuc1  6408  rdgisucinc  6409  rdgon  6410  frecabex  6422  frecabcl  6423  frecfcllem  6428  frecsuclem  6430  frecsuc  6431  frecrdg  6432  oav  6478  omv  6479  oeiv  6480  fvixp  6728  cbvixp  6740  mptelixpg  6759  elixpsn  6760  dom2lem  6797  xpcomco  6851  xpmapen  6877  fidceq  6896  fieq0  7004  ordiso2  7063  djune  7106  updjudhcoinlf  7108  updjudhcoinrg  7109  updjud  7110  omp1eom  7123  0ct  7135  ctmlemr  7136  ctssdclemn0  7138  ctssdccl  7139  ctssdc  7141  enumctlemm  7142  nnnninfeq  7155  nnnninfeq2  7156  enomnilem  7165  finomni  7167  fodjuomnilemdc  7171  fodju0  7174  fodjuomni  7176  ismkvnex  7182  fodjumkv  7187  nninfwlporlemd  7199  nninfwlpor  7201  exmidaclem  7236  cc1  7293  cc2lem  7294  cc2  7295  cc3  7296  mulpipq2  7399  genipv  7537  genpelxp  7539  addcanprleml  7642  addcanprlemu  7643  recexprlemm  7652  recexprlemdisj  7658  recexprlemloc  7659  recexprlem1ssl  7661  recexprlem1ssu  7662  cauappcvgprlemm  7673  cauappcvgprlemdisj  7679  cauappcvgprlemloc  7680  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  cauappcvgprlem1  7687  cauappcvgprlem2  7688  cauappcvgprlemlim  7689  cauappcvgpr  7690  caucvgprlemnkj  7694  caucvgprlemnbj  7695  caucvgprlemm  7696  caucvgprlemdisj  7702  caucvgprlemloc  7703  caucvgprlemcl  7704  caucvgprlemladdfu  7705  caucvgprlemladdrl  7706  caucvgprlem1  7707  caucvgprlem2  7708  caucvgpr  7710  caucvgprprlemell  7713  caucvgprprlemelu  7714  caucvgprprlemcbv  7715  caucvgprprlemval  7716  caucvgprprlemnkeqj  7718  caucvgprprlemnbj  7721  caucvgprprlemml  7722  caucvgprprlemmu  7723  caucvgprprlemopl  7725  caucvgprprlemlol  7726  caucvgprprlemopu  7727  caucvgprprlemloc  7731  caucvgprprlemclphr  7733  caucvgprprlemexbt  7734  caucvgprprlem1  7737  caucvgprprlem2  7738  caucvgsrlemcl  7817  caucvgsrlemfv  7819  caucvgsrlembound  7822  caucvgsrlemgt1  7823  caucvgsrlemoffval  7824  caucvgsrlemoffres  7828  caucvgsrlembnd  7829  caucvgsr  7830  axcaucvglemcau  7926  axcaucvglemres  7927  uz11  9579  cnref1o  9679  fzprval  10111  fztpval  10112  frec2uzuzd  10432  frec2uzltd  10433  frec2uzlt2d  10434  frecuzrdgrrn  10438  frec2uzrdg  10439  frecuzrdgtcl  10442  frecuzrdgg  10446  frecuzrdgfunlem  10449  frecfzennn  10456  seqeq1  10478  iseqovex  10486  seq3val  10488  seqvalcd  10489  seq3-1  10490  seqf  10491  seq3p1  10492  seqovcd  10493  seqp1cd  10496  seq3clss  10497  seq3fveq2  10499  seq3fveq  10501  seq3feq  10502  seq3shft2  10503  monoord  10506  monoord2  10507  ser3mono  10508  seq3split  10509  seq3caopr3  10511  seq3caopr2  10512  iseqf1olemkle  10514  iseqf1olemklt  10515  iseqf1olemqval  10517  iseqf1olemqk  10524  iseqf1olemjpcl  10525  iseqf1olemqpcl  10526  iseqf1olemfvp  10527  seq3f1olemqsumkj  10528  seq3f1olemqsum  10530  seq3f1olemstep  10531  seq3f1olemp  10532  seq3f1oleml  10533  seq3f1o  10534  seq3id2  10539  seq3homo  10540  seq3z  10541  ser3ge0  10547  ser3le  10548  exp3vallem  10551  exp3val  10552  facp1  10741  faccl  10746  facdiv  10749  facwordi  10751  faclbnd  10752  facubnd  10756  bcval  10760  bcval5  10774  fz1eqb  10801  omgadd  10813  hashxp  10837  zfz1isolem1  10851  zfz1iso  10852  seq3coll  10853  seq3shft  10878  reval  10889  replim  10899  cj11  10945  caucvgre  11021  cvg1nlemcau  11024  cvg1nlemres  11025  rexuz3  11030  absval  11041  resqrexlemover  11050  resqrexlemdecn  11052  resqrexlemlo  11053  resqrexlemcalc3  11056  resqrexlemnm  11058  resqrexlemcvg  11059  resqrexlemoverl  11061  resqrexlemglsq  11062  resqrexlemga  11063  resqrexlemsqa  11064  resqrexlemex  11065  abs00bd  11106  cau3lem  11154  caubnd2  11157  climconst  11329  climmpt  11339  climshftlemg  11341  climcn1  11347  climle  11373  climub  11383  climserle  11384  climcau  11386  climcvg1nlem  11388  climcvg1n  11389  serf0  11391  fsum3cvg  11417  summodclem3  11419  summodclem2a  11420  summodclem2  11421  summodc  11422  zsumdc  11423  fsum3  11426  fsumf1o  11429  fisumss  11431  fsum3cvg2  11433  fsum3ser  11436  fsumcl2lem  11437  fsumadd  11445  sumsnf  11448  isummulc2  11465  isumge0  11469  isumadd  11470  fsum2dlemstep  11473  fsummulc2  11487  fsumconst  11493  fsumrelem  11510  isumshft  11529  isum1p  11531  isumnn0nn  11532  isumrpcl  11533  isumlessdc  11535  cvgratnnlemnexp  11563  cvgratnnlemmn  11564  cvgratnnlemseq  11565  cvgratnnlemabsle  11566  cvgratnnlemfm  11568  cvgratnnlemrate  11569  cvgratnn  11570  cvgratz  11571  mertenslemi1  11574  mertenslem2  11575  mertensabs  11576  clim2prod  11578  prodfap0  11584  prodfrecap  11585  prodfdivap  11586  fproddccvg  11611  prodmodclem3  11614  prodmodclem2a  11615  prodmodclem2  11616  prodmodc  11617  zproddc  11618  fprodseq  11622  fprodf1o  11627  fprodssdc  11629  fprodmul  11630  prodsnf  11631  fprodfac  11654  fprodconst  11659  fprod2dlemstep  11661  eftvalcn  11696  ef0lem  11699  ege2le3  11710  efcj  11712  efaddlem  11713  eftlub  11729  efgt1p2  11734  reef11  11738  tanvalap  11747  efieq1re  11810  eirraplem  11815  dvdsabseq  11884  dvdsfac  11897  zsupcllemex  11978  infssuzex  11981  suprzubdc  11984  gcd0id  12011  nn0seqcvgd  12072  alginv  12078  algcvg  12079  algcvga  12082  algfx  12083  eucalglt  12088  lcmid  12111  qredeu  12128  prmfac1  12183  sqne2sq  12208  qnumdenbi  12223  dfphi2  12251  eulerthlemrprm  12260  eulerthlema  12261  eulerthlemh  12262  eulerthlemth  12263  phisum  12271  pcmpt  12374  pcfac  12381  1arithlem4  12397  elgz  12402  4sqlem4  12423  4sqlem12  12433  ennnfonelemk  12450  ennnfonelemp1  12456  ennnfoneleminc  12461  ennnfonelemkh  12462  ennnfonelemhf1o  12463  ennnfonelemex  12464  ennnfonelemhom  12465  ennnfonelemrn  12469  ennnfonelemnn0  12472  ennnfonelemr  12473  ennnfonelemim  12474  ctinfomlemom  12477  ctinfom  12478  ctiunctlemfo  12489  nninfdclemlt  12501  nninfdclemf1  12502  sloteq  12516  ressvalsets  12573  topnvalg  12753  imasex  12779  imasaddvallemg  12789  qusex  12799  xpsfrnel  12817  xpsfeq  12818  xpsval  12825  ismgm  12830  plusffvalg  12835  grpidvalg  12846  issgrp  12863  ismnddef  12876  ismhm  12910  mhmex  12911  mhmlin  12916  issubm  12921  mhmeql  12941  isgrp  12948  grpn0  12976  grpinvfvalg  12983  grpsubfvalg  12986  grpsubval  12987  grpinv11  13010  grpinvnz  13012  mhmlem  13053  mulgfvalg  13060  mulgsubcl  13073  mulgaddcomlem  13082  mulgneg2  13093  mulgass  13096  issubg  13109  subgex  13112  issubg2m  13125  issubg4m  13129  0subg  13135  isnsg  13138  releqgg  13156  eqgex  13157  eqgval  13159  isghm  13179  ghmlin  13184  ghmrn  13193  ghmeql  13203  f1ghm0to0  13208  iscmn  13229  mgpvalg  13274  isrng  13285  issrg  13316  srgfcl  13324  isring  13351  iscrng  13354  mulgass2  13407  opprvalg  13416  reldvdsrsrg  13439  dvdsrvald  13440  isunitd  13453  invrfvald  13469  dvrfvald  13480  dvrvald  13481  isrhm  13505  rhmval  13520  isnzr  13528  islring  13536  issubrng  13543  issubrg  13565  aprval  13595  aprap  13599  islmod  13604  scaffvalg  13619  lsssetm  13669  lspfval  13701  sraval  13750  rlmvalg  13767  2idlvalg  13814  cnfldmulg  13876  zlmval  13920  istps  13984  clsfval  14053  cnpval  14150  lmconst  14168  txcnp  14223  upxp  14224  uptx  14226  txlm  14231  lmcn2  14232  cnmpt11  14235  cnmpt11f  14236  cnmpt1t  14237  cnmpt21  14243  cnmpt21f  14244  cnmpt2t  14245  mopnval  14394  isxms  14403  isms  14405  comet  14451  mopnex  14457  xmetxp  14459  xmetxpbl  14460  txmetcnp  14470  txmetcn  14471  qtopbasss  14473  cncfi  14517  cncfmpt1f  14536  ivthinclemlm  14564  ivthinclemum  14565  ivthinclemlopn  14566  ivthinclemlr  14567  ivthinclemuopn  14568  ivthinclemur  14569  ivthinclemdisj  14570  ivthinclemloc  14571  ivthinc  14573  ivthdec  14574  cnlimci  14594  limccnpcntop  14596  eldvap  14603  dvcoapbr  14623  dvcj  14625  dvfre  14626  dvmptcjx  14638  dveflem  14639  sin0pilem2  14655  pilem3  14656  coseq0q4123  14707  coseq0negpitopi  14709  cos11  14726  logltb  14747  rpcxpef  14767  rplogbval  14815  zabsle1  14853  lgslem2  14855  lgslem3  14856  lgsfcl2  14860  lgsfle1  14863  lgsle1  14869  lgsdirprm  14888  lgseisenlem2  14904  2sqlem1  14914  2sqlem2  14915  mul2sq  14916  2sqlem3  14917  2sqlem9  14924  2sqlem10  14925  012of  15199  2o01f  15200  subctctexmid  15204  nnsf  15208  nninfalllem1  15211  nninffeq  15223  qdencn  15229  trilpolemclim  15238  trilpolemcl  15239  trilpolemisumle  15240  trilpolemeq1  15242  trilpolemlt1  15243  trilpo  15245  iswomni0  15253  redcwlpo  15257  dceqnconst  15262  dcapnconst  15263  nconstwlpolemgt0  15266  nconstwlpolem  15267  nconstwlpo  15268  neapmkv  15270