Theorem fveq2 5485

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 3984	. . 3 |- ( A = B -> ( A F x <-> B F x ) )
2	1	iotabidv 5173	. 2 |- ( A = B -> ( iota x A F x ) = ( iota x B F x ) )
3		df-fv 5195	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5195	. 2 |- ( F ` B ) = ( iota x B F x )
5	2, 3, 4	3eqtr4g 2223	1 |- ( A = B -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1343   class class class wbr 3981   iotacio 5150   ` cfv 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195

This theorem is referenced by:  fveq2i  5488  fveq2d  5489  2fveq3  5490  fvifdc  5507  dffn5imf  5540  fvelimab  5541  ssimaex  5546  fvco4  5557  fvmptssdm  5569  fvmptf  5577  eqfnfv2f  5586  fvelrn  5615  ralrnmpt  5626  rexrnmpt  5627  ffnfvf  5643  fmptco  5650  cofmpt  5653  fcompt  5654  fcoconst  5655  fnressn  5670  fressnfv  5671  fconstfvm  5702  foco2  5721  funiunfvdmf  5731  f1veqaeq  5736  dff13f  5737  f1fveq  5739  f1elima  5740  f1ocnvfv  5746  f1ocnvfvb  5747  fcofo  5751  cocan2  5755  fliftfun  5763  isorel  5775  isocnv  5778  isotr  5783  f1oiso2  5794  canth  5795  imbrov2fvoveq  5866  ffnov  5942  eqfnov  5944  fnovim  5946  fnrnov  5983  foov  5984  funimassov  5987  ovelimab  5988  suppssfv  6045  ofvalg  6058  ofrval  6059  offval2  6064  ofrfval2  6065  ofco  6067  caofinvl  6071  op1std  6113  op2ndd  6114  1stval2  6120  2ndval2  6121  unielxp  6139  reldm  6151  oprabco  6181  2ndconst  6186  f1o2ndf1  6192  mpoxopn0yelv  6203  mpoxopoveq  6204  smoel  6264  tfrlem1  6272  tfrlem3-2d  6276  tfrlem5  6278  tfrlem9  6283  tfr0dm  6286  tfrlemiubacc  6294  tfrlemi1  6296  tfrexlem  6298  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemubacc  6310  tfr1onlemaccex  6312  tfr1onlemres  6313  tfri1dALT  6315  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemubacc  6323  tfrcllemaccex  6325  tfrcllemres  6326  tfrcldm  6327  tfrcl  6328  tfri3  6331  rdgtfr  6338  rdgss  6347  rdgisuc1  6348  rdgisucinc  6349  rdgon  6350  frecabex  6362  frecabcl  6363  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  frecrdg  6372  oav  6418  omv  6419  oeiv  6420  fvixp  6665  cbvixp  6677  mptelixpg  6696  elixpsn  6697  dom2lem  6734  xpcomco  6788  xpmapen  6812  fidceq  6831  fieq0  6937  ordiso2  6996  djune  7039  updjudhcoinlf  7041  updjudhcoinrg  7042  updjud  7043  omp1eom  7056  0ct  7068  ctmlemr  7069  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumctlemm  7075  nnnninfeq  7088  nnnninfeq2  7089  enomnilem  7098  finomni  7100  fodjuomnilemdc  7104  fodju0  7107  fodjuomni  7109  ismkvnex  7115  fodjumkv  7120  exmidaclem  7160  cc1  7202  cc2lem  7203  cc2  7204  cc3  7205  mulpipq2  7308  genipv  7446  genpelxp  7448  addcanprleml  7551  addcanprlemu  7552  recexprlemm  7561  recexprlemdisj  7567  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  cauappcvgprlemm  7582  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprlem2  7617  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkeqj  7627  caucvgprprlemnbj  7630  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlem1  7646  caucvgprprlem2  7647  caucvgsrlemcl  7726  caucvgsrlemfv  7728  caucvgsrlembound  7731  caucvgsrlemgt1  7732  caucvgsrlemoffval  7733  caucvgsrlemoffres  7737  caucvgsrlembnd  7738  caucvgsr  7739  axcaucvglemcau  7835  axcaucvglemres  7836  uz11  9484  cnref1o  9584  fzprval  10013  fztpval  10014  frec2uzuzd  10333  frec2uzltd  10334  frec2uzlt2d  10335  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgtcl  10343  frecuzrdgg  10347  frecuzrdgfunlem  10350  frecfzennn  10357  seqeq1  10379  iseqovex  10387  seq3val  10389  seqvalcd  10390  seq3-1  10391  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3clss  10398  seq3fveq2  10400  seq3fveq  10402  seq3feq  10403  seq3shft2  10404  monoord  10407  monoord2  10408  ser3mono  10409  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqval  10418  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1olemp  10433  seq3f1oleml  10434  seq3f1o  10435  seq3id2  10440  seq3homo  10441  seq3z  10442  ser3ge0  10448  ser3le  10449  exp3vallem  10452  exp3val  10453  facp1  10639  faccl  10644  facdiv  10647  facwordi  10649  faclbnd  10650  facubnd  10654  bcval  10658  bcval5  10672  fz1eqb  10700  omgadd  10711  hashxp  10735  zfz1isolem1  10749  zfz1iso  10750  seq3coll  10751  seq3shft  10776  reval  10787  replim  10797  cj11  10843  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  rexuz3  10928  absval  10939  resqrexlemover  10948  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  resqrexlemsqa  10962  resqrexlemex  10963  abs00bd  11004  cau3lem  11052  caubnd2  11055  climconst  11227  climmpt  11237  climshftlemg  11239  climcn1  11245  climle  11271  climub  11281  climserle  11282  climcau  11284  climcvg1nlem  11286  climcvg1n  11287  serf0  11289  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  summodclem2  11319  summodc  11320  zsumdc  11321  fsum3  11324  fsumf1o  11327  fisumss  11329  fsum3cvg2  11331  fsum3ser  11334  fsumcl2lem  11335  fsumadd  11343  sumsnf  11346  isummulc2  11363  isumge0  11367  isumadd  11368  fsum2dlemstep  11371  fsummulc2  11385  fsumconst  11391  fsumrelem  11408  isumshft  11427  isum1p  11429  isumnn0nn  11430  isumrpcl  11431  isumlessdc  11433  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratnn  11468  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2prod  11476  prodfap0  11482  prodfrecap  11483  prodfdivap  11484  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodf1o  11525  fprodssdc  11527  fprodmul  11528  prodsnf  11529  fprodfac  11552  fprodconst  11557  fprod2dlemstep  11559  eftvalcn  11594  ef0lem  11597  ege2le3  11608  efcj  11610  efaddlem  11611  eftlub  11627  efgt1p2  11632  reef11  11636  tanvalap  11645  efieq1re  11708  eirraplem  11713  dvdsabseq  11781  dvdsfac  11794  zsupcllemex  11875  infssuzex  11878  suprzubdc  11881  gcd0id  11908  nn0seqcvgd  11969  alginv  11975  algcvg  11976  algcvga  11979  algfx  11980  eucalglt  11985  lcmid  12008  qredeu  12025  prmfac1  12080  sqne2sq  12105  qnumdenbi  12120  dfphi2  12148  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  phisum  12168  pcmpt  12269  pcfac  12276  1arithlem4  12292  elgz  12297  4sqlem4  12318  ennnfonelemk  12329  ennnfonelemp1  12335  ennnfoneleminc  12340  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemrn  12348  ennnfonelemnn0  12351  ennnfonelemr  12352  ennnfonelemim  12353  ctinfomlemom  12356  ctinfom  12357  ctiunctlemfo  12368  nninfdclemlt  12380  nninfdclemf1  12381  sloteq  12395  topnvalg  12563  istps  12630  clsfval  12701  cnpval  12798  lmconst  12816  txcnp  12871  upxp  12872  uptx  12874  txlm  12879  lmcn2  12880  cnmpt11  12883  cnmpt11f  12884  cnmpt1t  12885  cnmpt21  12891  cnmpt21f  12892  cnmpt2t  12893  mopnval  13042  isxms  13051  isms  13053  comet  13099  mopnex  13105  xmetxp  13107  xmetxpbl  13108  txmetcnp  13118  txmetcn  13119  qtopbasss  13121  cncfi  13165  cncfmpt1f  13184  ivthinclemlm  13212  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  ivthinc  13221  ivthdec  13222  cnlimci  13242  limccnpcntop  13244  eldvap  13251  dvcoapbr  13271  dvcj  13273  dvfre  13274  dvmptcjx  13286  dveflem  13287  sin0pilem2  13303  pilem3  13304  coseq0q4123  13355  coseq0negpitopi  13357  cos11  13374  logltb  13395  rpcxpef  13415  rplogbval  13463  zabsle1  13500  lgslem2  13502  lgslem3  13503  lgsfcl2  13507  lgsfle1  13510  lgsle1  13516  lgsdirprm  13535  2sqlem1  13550  2sqlem2  13551  mul2sq  13552  2sqlem3  13553  2sqlem9  13560  2sqlem10  13561  012of  13835  2o01f  13836  subctctexmid  13841  nnsf  13845  nninfalllem1  13848  nninffeq  13860  qdencn  13866  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trilpo  13882  iswomni0  13890  redcwlpo  13894  dceqnconst  13898  dcapnconst  13899  nconstwlpolemgt0  13902  nconstwlpolem  13903  nconstwlpo  13904  neapmkv  13906