Theorem fveq2 5515

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 4006	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5199	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5224	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5224	. 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 4003   iotacio 5176   ` cfv 5216

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  fveq2i  5518  fveq2d  5519  2fveq3  5520  fvifdc  5537  dffn5imf  5571  fvelimab  5572  ssimaex  5577  fvco4  5588  fvmptssdm  5600  fvmptf  5608  eqfnfv2f  5617  fvelrn  5647  ralrnmpt  5658  rexrnmpt  5659  ffnfvf  5675  fmptco  5682  cofmpt  5685  fcompt  5686  fcoconst  5687  fnressn  5702  fressnfv  5703  fconstfvm  5734  foco2  5754  funiunfvdmf  5764  f1veqaeq  5769  dff13f  5770  f1fveq  5772  f1elima  5773  f1ocnvfv  5779  f1ocnvfvb  5780  fcofo  5784  cocan2  5788  fliftfun  5796  isorel  5808  isocnv  5811  isotr  5816  f1oiso2  5827  canth  5828  imbrov2fvoveq  5899  ffnov  5978  eqfnov  5980  fnovim  5982  fnrnov  6019  foov  6020  funimassov  6023  ovelimab  6024  suppssfv  6078  ofvalg  6091  ofrval  6092  offval2  6097  ofrfval2  6098  ofco  6100  caofinvl  6104  op1std  6148  op2ndd  6149  1stval2  6155  2ndval2  6156  unielxp  6174  reldm  6186  oprabco  6217  2ndconst  6222  f1o2ndf1  6228  mpoxopn0yelv  6239  mpoxopoveq  6240  smoel  6300  tfrlem1  6308  tfrlem3-2d  6312  tfrlem5  6314  tfrlem9  6319  tfr0dm  6322  tfrlemiubacc  6330  tfrlemi1  6332  tfrexlem  6334  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemaccex  6348  tfr1onlemres  6349  tfri1dALT  6351  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemaccex  6361  tfrcllemres  6362  tfrcldm  6363  tfrcl  6364  tfri3  6367  rdgtfr  6374  rdgss  6383  rdgisuc1  6384  rdgisucinc  6385  rdgon  6386  frecabex  6398  frecabcl  6399  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  frecrdg  6408  oav  6454  omv  6455  oeiv  6456  fvixp  6702  cbvixp  6714  mptelixpg  6733  elixpsn  6734  dom2lem  6771  xpcomco  6825  xpmapen  6849  fidceq  6868  fieq0  6974  ordiso2  7033  djune  7076  updjudhcoinlf  7078  updjudhcoinrg  7079  updjud  7080  omp1eom  7093  0ct  7105  ctmlemr  7106  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumctlemm  7112  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  finomni  7137  fodjuomnilemdc  7141  fodju0  7144  fodjuomni  7146  ismkvnex  7152  fodjumkv  7157  nninfwlporlemd  7169  nninfwlpor  7171  exmidaclem  7206  cc1  7263  cc2lem  7264  cc2  7265  cc3  7266  mulpipq2  7369  genipv  7507  genpelxp  7509  addcanprleml  7612  addcanprlemu  7613  recexprlemm  7622  recexprlemdisj  7628  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  cauappcvgprlemm  7643  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlem2  7658  cauappcvgprlemlim  7659  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgsrlemcl  7787  caucvgsrlemfv  7789  caucvgsrlembound  7792  caucvgsrlemgt1  7793  caucvgsrlemoffval  7794  caucvgsrlemoffres  7798  caucvgsrlembnd  7799  caucvgsr  7800  axcaucvglemcau  7896  axcaucvglemres  7897  uz11  9549  cnref1o  9649  fzprval  10081  fztpval  10082  frec2uzuzd  10401  frec2uzltd  10402  frec2uzlt2d  10403  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgtcl  10411  frecuzrdgg  10415  frecuzrdgfunlem  10418  frecfzennn  10425  seqeq1  10447  iseqovex  10455  seq3val  10457  seqvalcd  10458  seq3-1  10459  seqf  10460  seq3p1  10461  seqovcd  10462  seqp1cd  10465  seq3clss  10466  seq3fveq2  10468  seq3fveq  10470  seq3feq  10471  seq3shft2  10472  monoord  10475  monoord2  10476  ser3mono  10477  seq3split  10478  seq3caopr3  10480  seq3caopr2  10481  iseqf1olemkle  10483  iseqf1olemklt  10484  iseqf1olemqval  10486  iseqf1olemqk  10493  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsum  10499  seq3f1olemstep  10500  seq3f1olemp  10501  seq3f1oleml  10502  seq3f1o  10503  seq3id2  10508  seq3homo  10509  seq3z  10510  ser3ge0  10516  ser3le  10517  exp3vallem  10520  exp3val  10521  facp1  10709  faccl  10714  facdiv  10717  facwordi  10719  faclbnd  10720  facubnd  10724  bcval  10728  bcval5  10742  fz1eqb  10769  omgadd  10781  hashxp  10805  zfz1isolem1  10819  zfz1iso  10820  seq3coll  10821  seq3shft  10846  reval  10857  replim  10867  cj11  10913  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  rexuz3  10998  absval  11009  resqrexlemover  11018  resqrexlemdecn  11020  resqrexlemlo  11021  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  resqrexlemsqa  11032  resqrexlemex  11033  abs00bd  11074  cau3lem  11122  caubnd2  11125  climconst  11297  climmpt  11307  climshftlemg  11309  climcn1  11315  climle  11341  climub  11351  climserle  11352  climcau  11354  climcvg1nlem  11356  climcvg1n  11357  serf0  11359  fsum3cvg  11385  summodclem3  11387  summodclem2a  11388  summodclem2  11389  summodc  11390  zsumdc  11391  fsum3  11394  fsumf1o  11397  fisumss  11399  fsum3cvg2  11401  fsum3ser  11404  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  isummulc2  11433  isumge0  11437  isumadd  11438  fsum2dlemstep  11441  fsummulc2  11455  fsumconst  11461  fsumrelem  11478  isumshft  11497  isum1p  11499  isumnn0nn  11500  isumrpcl  11501  isumlessdc  11503  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemseq  11533  cvgratnnlemabsle  11534  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratnn  11538  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  clim2prod  11546  prodfap0  11552  prodfrecap  11553  prodfdivap  11554  fproddccvg  11579  prodmodclem3  11582  prodmodclem2a  11583  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodseq  11590  fprodf1o  11595  fprodssdc  11597  fprodmul  11598  prodsnf  11599  fprodfac  11622  fprodconst  11627  fprod2dlemstep  11629  eftvalcn  11664  ef0lem  11667  ege2le3  11678  efcj  11680  efaddlem  11681  eftlub  11697  efgt1p2  11702  reef11  11706  tanvalap  11715  efieq1re  11778  eirraplem  11783  dvdsabseq  11852  dvdsfac  11865  zsupcllemex  11946  infssuzex  11949  suprzubdc  11952  gcd0id  11979  nn0seqcvgd  12040  alginv  12046  algcvg  12047  algcvga  12050  algfx  12051  eucalglt  12056  lcmid  12079  qredeu  12096  prmfac1  12151  sqne2sq  12176  qnumdenbi  12191  dfphi2  12219  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  phisum  12239  pcmpt  12340  pcfac  12347  1arithlem4  12363  elgz  12368  4sqlem4  12389  ennnfonelemk  12400  ennnfonelemp1  12406  ennnfoneleminc  12411  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemrn  12419  ennnfonelemnn0  12422  ennnfonelemr  12423  ennnfonelemim  12424  ctinfomlemom  12427  ctinfom  12428  ctiunctlemfo  12439  nninfdclemlt  12451  nninfdclemf1  12452  sloteq  12466  ressvalsets  12523  topnvalg  12699  imasex  12725  imasaddvallemg  12735  xpsfrnel  12762  xpsfeq  12763  xpsval  12770  ismgm  12775  plusffvalg  12780  grpidvalg  12791  issgrp  12808  ismnddef  12818  ismhm  12852  mhmlin  12857  issubm  12862  mhmeql  12875  isgrp  12882  grpn0  12907  grpinvfvalg  12914  grpsubfvalg  12917  grpsubval  12918  grpinv11  12938  grpinvnz  12940  mhmlem  12977  mulgfvalg  12984  mulgsubcl  12996  mulgaddcomlem  13004  mulgneg2  13015  mulgass  13018  issubg  13031  subgex  13034  issubg2m  13047  issubg4m  13051  0subg  13057  isnsg  13060  releqgg  13078  eqgval  13080  iscmn  13094  mgpvalg  13131  issrg  13146  srgfcl  13154  isring  13181  iscrng  13184  mulgass2  13233  opprvalg  13239  reldvdsrsrg  13259  dvdsrvald  13260  isunitd  13273  invrfvald  13289  dvrfvald  13300  dvrvald  13301  isnzr  13323  islring  13331  issubrg  13340  aprval  13370  aprap  13374  islmod  13379  scaffvalg  13394  cnfldmulg  13440  istps  13502  clsfval  13571  cnpval  13668  lmconst  13686  txcnp  13741  upxp  13742  uptx  13744  txlm  13749  lmcn2  13750  cnmpt11  13753  cnmpt11f  13754  cnmpt1t  13755  cnmpt21  13761  cnmpt21f  13762  cnmpt2t  13763  mopnval  13912  isxms  13921  isms  13923  comet  13969  mopnex  13975  xmetxp  13977  xmetxpbl  13978  txmetcnp  13988  txmetcn  13989  qtopbasss  13991  cncfi  14035  cncfmpt1f  14054  ivthinclemlm  14082  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  ivthinc  14091  ivthdec  14092  cnlimci  14112  limccnpcntop  14114  eldvap  14121  dvcoapbr  14141  dvcj  14143  dvfre  14144  dvmptcjx  14156  dveflem  14157  sin0pilem2  14173  pilem3  14174  coseq0q4123  14225  coseq0negpitopi  14227  cos11  14244  logltb  14265  rpcxpef  14285  rplogbval  14333  zabsle1  14370  lgslem2  14372  lgslem3  14373  lgsfcl2  14377  lgsfle1  14380  lgsle1  14386  lgsdirprm  14405  lgseisenlem2  14421  2sqlem1  14431  2sqlem2  14432  mul2sq  14433  2sqlem3  14434  2sqlem9  14441  2sqlem10  14442  012of  14715  2o01f  14716  subctctexmid  14720  nnsf  14724  nninfalllem1  14727  nninffeq  14739  qdencn  14745  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trilpo  14761  iswomni0  14769  redcwlpo  14773  dceqnconst  14777  dcapnconst  14778  nconstwlpolemgt0  14781  nconstwlpolem  14782  nconstwlpo  14783  neapmkv  14785