Theorem fveq2 5558

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 4036	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5241	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5266	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5266	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4033   iotacio 5217   ` cfv 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266

This theorem is referenced by:  fveq2i  5561  fveq2d  5562  2fveq3  5563  fvifdc  5580  dffn5imf  5616  fvelimab  5617  ssimaex  5622  fvco4  5633  fvmptssdm  5646  fvmptf  5654  eqfnfv2f  5663  fvelrn  5693  ralrnmpt  5704  rexrnmpt  5705  ffnfvf  5721  fmptco  5728  cofmpt  5731  fcompt  5732  fcoconst  5733  fnressn  5748  fressnfv  5749  fconstfvm  5780  foco2  5800  funiunfvdmf  5811  f1veqaeq  5816  dff13f  5817  f1fveq  5819  f1elima  5820  f1ocnvfv  5826  f1ocnvfvb  5827  fcofo  5831  cocan2  5835  fliftfun  5843  isorel  5855  isocnv  5858  isotr  5863  f1oiso2  5874  canth  5875  imbrov2fvoveq  5947  ffnov  6026  eqfnov  6029  fnovim  6031  fnrnov  6069  foov  6070  funimassov  6073  ovelimab  6074  suppssfv  6131  ofvalg  6145  ofrval  6146  offval2  6151  ofrfval2  6152  ofco  6154  caofinvl  6160  op1std  6206  op2ndd  6207  1stval2  6213  2ndval2  6214  unielxp  6232  reldm  6244  oprabco  6275  2ndconst  6280  f1o2ndf1  6286  mpoxopn0yelv  6297  mpoxopoveq  6298  smoel  6358  tfrlem1  6366  tfrlem3-2d  6370  tfrlem5  6372  tfrlem9  6377  tfr0dm  6380  tfrlemiubacc  6388  tfrlemi1  6390  tfrexlem  6392  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemubacc  6404  tfr1onlemaccex  6406  tfr1onlemres  6407  tfri1dALT  6409  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemubacc  6417  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  tfrcl  6422  tfri3  6425  rdgtfr  6432  rdgss  6441  rdgisuc1  6442  rdgisucinc  6443  rdgon  6444  frecabex  6456  frecabcl  6457  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  frecrdg  6466  oav  6512  omv  6513  oeiv  6514  fvixp  6762  cbvixp  6774  mptelixpg  6793  elixpsn  6794  dom2lem  6831  xpcomco  6885  xpmapen  6911  fidceq  6930  fieq0  7042  ordiso2  7101  djune  7144  updjudhcoinlf  7146  updjudhcoinrg  7147  updjud  7148  omp1eom  7161  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  finomni  7206  fodjuomnilemdc  7210  fodju0  7213  fodjuomni  7215  ismkvnex  7221  fodjumkv  7226  nninfwlporlemd  7238  nninfwlpor  7240  exmidaclem  7275  cc1  7332  cc2lem  7333  cc2  7334  cc3  7335  mulpipq2  7438  genipv  7576  genpelxp  7578  addcanprleml  7681  addcanprlemu  7682  recexprlemm  7691  recexprlemdisj  7697  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  cauappcvgprlemm  7712  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlem2  7727  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemnbj  7760  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsrlembound  7861  caucvgsrlemgt1  7862  caucvgsrlemoffval  7863  caucvgsrlemoffres  7867  caucvgsrlembnd  7868  caucvgsr  7869  axcaucvglemcau  7965  axcaucvglemres  7966  uz11  9624  cnref1o  9725  fzprval  10157  fztpval  10158  zsupcllemex  10320  infssuzex  10323  suprzubdc  10326  frec2uzuzd  10494  frec2uzltd  10495  frec2uzlt2d  10496  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgtcl  10504  frecuzrdgg  10508  frecuzrdgfunlem  10511  frecfzennn  10518  seqeq1  10542  iseqovex  10550  seq3val  10552  seqvalcd  10553  seq3-1  10554  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3clss  10563  seq3fveq2  10567  seqfveq2g  10569  seqfveqg  10570  seq3fveq  10571  seq3feq  10572  seq3shft2  10573  seqshft2g  10574  monoord  10577  monoord2  10578  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqval  10592  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1olemp  10607  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem2a  10610  seqf1og  10613  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  ser3le  10629  exp3vallem  10632  exp3val  10633  facp1  10822  faccl  10827  facdiv  10830  facwordi  10832  faclbnd  10833  facubnd  10837  bcval  10841  bcval5  10855  fz1eqb  10882  omgadd  10894  hashxp  10918  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  eqwrd  10975  seq3shft  11003  reval  11014  replim  11024  cj11  11070  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  rexuz3  11155  absval  11166  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  resqrexlemsqa  11189  resqrexlemex  11190  abs00bd  11231  cau3lem  11279  caubnd2  11282  climconst  11455  climmpt  11465  climshftlemg  11467  climcn1  11473  climle  11499  climub  11509  climserle  11510  climcau  11512  climcvg1nlem  11514  climcvg1n  11515  serf0  11517  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  fsumf1o  11555  fisumss  11557  fsum3cvg2  11559  fsum3ser  11562  fsumcl2lem  11563  fsumadd  11571  sumsnf  11574  isummulc2  11591  isumge0  11595  isumadd  11596  fsum2dlemstep  11599  fsummulc2  11613  fsumconst  11619  fsumrelem  11636  isumshft  11655  isum1p  11657  isumnn0nn  11658  isumrpcl  11659  isumlessdc  11661  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  clim2prod  11704  prodfap0  11710  prodfrecap  11711  prodfdivap  11712  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  prodsnf  11757  fprodfac  11780  fprodconst  11785  fprod2dlemstep  11787  eftvalcn  11822  ef0lem  11825  ege2le3  11836  efcj  11838  efaddlem  11839  eftlub  11855  efgt1p2  11860  reef11  11864  tanvalap  11873  efieq1re  11937  eirraplem  11942  dvdsabseq  12012  dvdsfac  12025  gcd0id  12146  nninfctlemfo  12207  nn0seqcvgd  12209  alginv  12215  algcvg  12216  algcvga  12219  algfx  12220  eucalglt  12225  lcmid  12248  qredeu  12265  prmfac1  12320  sqne2sq  12345  qnumdenbi  12360  dfphi2  12388  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  phisum  12409  pcmpt  12512  pcfac  12519  1arithlem4  12535  elgz  12540  4sqlem4  12561  4sqlem12  12571  2expltfac  12608  ennnfonelemk  12617  ennnfonelemp1  12623  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemrn  12636  ennnfonelemnn0  12639  ennnfonelemr  12640  ennnfonelemim  12641  ctinfomlemom  12644  ctinfom  12645  ctiunctlemfo  12656  nninfdclemlt  12668  nninfdclemf1  12669  sloteq  12683  ressvalsets  12742  topnvalg  12922  imasex  12948  imasaddvallemg  12958  qusex  12968  xpsfrnel  12987  xpsfeq  12988  xpsval  12995  ismgm  13000  plusffvalg  13005  grpidvalg  13016  gsumfzval  13034  gsumval2  13040  issgrp  13046  ismnddef  13059  ismhm  13093  mhmex  13094  mhmlin  13099  issubm  13104  mhmeql  13124  isgrp  13138  grpn0  13167  grpinvfvalg  13174  grpsubfvalg  13177  grpsubval  13178  grpinv11  13201  grpinvnz  13203  mhmlem  13244  mulgfvalg  13251  mulgsubcl  13266  mulgaddcomlem  13275  mulgneg2  13286  mulgass  13289  issubg  13303  subgex  13306  issubg2m  13319  issubg4m  13323  0subg  13329  isnsg  13332  releqgg  13350  eqgex  13351  eqgval  13353  isghm  13373  ghmlin  13378  ghmrn  13387  ghmeql  13397  f1ghm0to0  13402  iscmn  13423  mgpvalg  13479  isrng  13490  issrg  13521  srgfcl  13529  isring  13556  iscrng  13559  mulgass2  13614  opprvalg  13625  reldvdsrsrg  13648  dvdsrvald  13649  isunitd  13662  invrfvald  13678  dvrfvald  13689  dvrvald  13690  isrhm  13714  rhmval  13729  isnzr  13737  islring  13748  issubrng  13755  issubrg  13777  rrgval  13818  isdomn  13825  aprval  13838  aprap  13842  islmod  13847  scaffvalg  13862  lsssetm  13912  lspfval  13944  sraval  13993  rlmvalg  14010  2idlval  14058  2idlvalg  14059  cnfldmulg  14132  zlmval  14183  znf1o  14207  istps  14268  clsfval  14337  cnpval  14434  lmconst  14452  txcnp  14507  upxp  14508  uptx  14510  txlm  14515  lmcn2  14516  cnmpt11  14519  cnmpt11f  14520  cnmpt1t  14521  cnmpt21  14527  cnmpt21f  14528  cnmpt2t  14529  mopnval  14678  isxms  14687  isms  14689  comet  14735  mopnex  14741  xmetxp  14743  xmetxpbl  14744  txmetcnp  14754  txmetcn  14755  qtopbasss  14757  cncfi  14814  cncfmpt1f  14834  ivthinclemlm  14870  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthdec  14880  ivthreinc  14881  cnlimci  14909  limccnpcntop  14911  eldvap  14918  dvcoapbr  14943  dvcj  14945  dvfre  14946  dvmptcjx  14960  dveflem  14962  elply2  14971  elplyd  14977  plymullem1  14984  plyadd  14987  plymul  14988  plycoeid3  14993  plycolemc  14994  plyco  14995  plycjlemc  14996  plycj  14997  dvply1  15001  sin0pilem2  15018  pilem3  15019  coseq0q4123  15070  coseq0negpitopi  15072  cos11  15089  logltb  15110  rpcxpef  15130  rplogbval  15181  mpodvdsmulf1o  15226  fsumdvdsmul  15227  zabsle1  15240  lgslem2  15242  lgslem3  15243  lgsfcl2  15247  lgsfle1  15250  lgsle1  15256  lgsdirprm  15275  lgseisenlem2  15312  lgsquadlem2  15319  2sqlem1  15355  2sqlem2  15356  mul2sq  15357  2sqlem3  15358  2sqlem9  15365  2sqlem10  15366  012of  15640  2o01f  15641  subctctexmid  15645  nnsf  15649  nninfalllem1  15652  nninffeq  15664  qdencn  15671  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trilpo  15687  iswomni0  15695  redcwlpo  15699  dceqnconst  15704  dcapnconst  15705  nconstwlpolemgt0  15708  nconstwlpolem  15709  nconstwlpo  15710  neapmkv  15712