Theorem fveq2 5515

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq2	⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 4006	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5199	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5224	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5224	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2235	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4003  ℩cio 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  9548  cnref1o  9648  fzprval  10079  fztpval  10080  frec2uzuzd  10399  frec2uzltd  10400  frec2uzlt2d  10401  frecuzrdgrrn  10405  frec2uzrdg  10406  frecuzrdgtcl  10409  frecuzrdgg  10413  frecuzrdgfunlem  10416  frecfzennn  10423  seqeq1  10445  iseqovex  10453  seq3val  10455  seqvalcd  10456  seq3-1  10457  seqf  10458  seq3p1  10459  seqovcd  10460  seqp1cd  10463  seq3clss  10464  seq3fveq2  10466  seq3fveq  10468  seq3feq  10469  seq3shft2  10470  monoord  10473  monoord2  10474  ser3mono  10475  seq3split  10476  seq3caopr3  10478  seq3caopr2  10479  iseqf1olemkle  10481  iseqf1olemklt  10482  iseqf1olemqval  10484  iseqf1olemqk  10491  iseqf1olemjpcl  10492  iseqf1olemqpcl  10493  iseqf1olemfvp  10494  seq3f1olemqsumkj  10495  seq3f1olemqsum  10497  seq3f1olemstep  10498  seq3f1olemp  10499  seq3f1oleml  10500  seq3f1o  10501  seq3id2  10506  seq3homo  10507  seq3z  10508  ser3ge0  10514  ser3le  10515  exp3vallem  10518  exp3val  10519  facp1  10705  faccl  10710  facdiv  10713  facwordi  10715  faclbnd  10716  facubnd  10720  bcval  10724  bcval5  10738  fz1eqb  10765  omgadd  10777  hashxp  10801  zfz1isolem1  10815  zfz1iso  10816  seq3coll  10817  seq3shft  10842  reval  10853  replim  10863  cj11  10909  caucvgre  10985  cvg1nlemcau  10988  cvg1nlemres  10989  rexuz3  10994  absval  11005  resqrexlemover  11014  resqrexlemdecn  11016  resqrexlemlo  11017  resqrexlemcalc3  11020  resqrexlemnm  11022  resqrexlemcvg  11023  resqrexlemoverl  11025  resqrexlemglsq  11026  resqrexlemga  11027  resqrexlemsqa  11028  resqrexlemex  11029  abs00bd  11070  cau3lem  11118  caubnd2  11121  climconst  11293  climmpt  11303  climshftlemg  11305  climcn1  11311  climle  11337  climub  11347  climserle  11348  climcau  11350  climcvg1nlem  11352  climcvg1n  11353  serf0  11355  fsum3cvg  11381  summodclem3  11383  summodclem2a  11384  summodclem2  11385  summodc  11386  zsumdc  11387  fsum3  11390  fsumf1o  11393  fisumss  11395  fsum3cvg2  11397  fsum3ser  11400  fsumcl2lem  11401  fsumadd  11409  sumsnf  11412  isummulc2  11429  isumge0  11433  isumadd  11434  fsum2dlemstep  11437  fsummulc2  11451  fsumconst  11457  fsumrelem  11474  isumshft  11493  isum1p  11495  isumnn0nn  11496  isumrpcl  11497  isumlessdc  11499  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  cvgratnnlemseq  11529  cvgratnnlemabsle  11530  cvgratnnlemfm  11532  cvgratnnlemrate  11533  cvgratnn  11534  cvgratz  11535  mertenslemi1  11538  mertenslem2  11539  mertensabs  11540  clim2prod  11542  prodfap0  11548  prodfrecap  11549  prodfdivap  11550  fproddccvg  11575  prodmodclem3  11578  prodmodclem2a  11579  prodmodclem2  11580  prodmodc  11581  zproddc  11582  fprodseq  11586  fprodf1o  11591  fprodssdc  11593  fprodmul  11594  prodsnf  11595  fprodfac  11618  fprodconst  11623  fprod2dlemstep  11625  eftvalcn  11660  ef0lem  11663  ege2le3  11674  efcj  11676  efaddlem  11677  eftlub  11693  efgt1p2  11698  reef11  11702  tanvalap  11711  efieq1re  11774  eirraplem  11779  dvdsabseq  11847  dvdsfac  11860  zsupcllemex  11941  infssuzex  11944  suprzubdc  11947  gcd0id  11974  nn0seqcvgd  12035  alginv  12041  algcvg  12042  algcvga  12045  algfx  12046  eucalglt  12051  lcmid  12074  qredeu  12091  prmfac1  12146  sqne2sq  12171  qnumdenbi  12186  dfphi2  12214  eulerthlemrprm  12223  eulerthlema  12224  eulerthlemh  12225  eulerthlemth  12226  phisum  12234  pcmpt  12335  pcfac  12342  1arithlem4  12358  elgz  12363  4sqlem4  12384  ennnfonelemk  12395  ennnfonelemp1  12401  ennnfoneleminc  12406  ennnfonelemkh  12407  ennnfonelemhf1o  12408  ennnfonelemex  12409  ennnfonelemhom  12410  ennnfonelemrn  12414  ennnfonelemnn0  12417  ennnfonelemr  12418  ennnfonelemim  12419  ctinfomlemom  12422  ctinfom  12423  ctiunctlemfo  12434  nninfdclemlt  12446  nninfdclemf1  12447  sloteq  12461  ressvalsets  12518  topnvalg  12694  imasex  12720  imasaddvallemg  12730  xpsfrnel  12757  xpsfeq  12758  xpsval  12765  ismgm  12770  plusffvalg  12775  grpidvalg  12786  issgrp  12803  ismnddef  12813  ismhm  12847  mhmlin  12852  issubm  12857  mhmeql  12870  isgrp  12877  grpn0  12902  grpinvfvalg  12909  grpsubfvalg  12912  grpsubval  12913  grpinv11  12933  grpinvnz  12935  mhmlem  12972  mulgfvalg  12979  mulgsubcl  12991  mulgaddcomlem  12999  mulgneg2  13010  mulgass  13013  issubg  13026  subgex  13029  issubg2m  13042  issubg4m  13046  0subg  13052  isnsg  13055  releqgg  13073  eqgval  13075  iscmn  13089  mgpvalg  13126  issrg  13141  srgfcl  13149  isring  13176  iscrng  13179  mulgass2  13228  opprvalg  13234  reldvdsrsrg  13254  dvdsrvald  13255  isunitd  13268  invrfvald  13284  dvrfvald  13295  dvrvald  13296  isnzr  13318  islring  13326  aprval  13333  aprap  13337  issubrg  13342  cnfldmulg  13401  istps  13463  clsfval  13532  cnpval  13629  lmconst  13647  txcnp  13702  upxp  13703  uptx  13705  txlm  13710  lmcn2  13711  cnmpt11  13714  cnmpt11f  13715  cnmpt1t  13716  cnmpt21  13722  cnmpt21f  13723  cnmpt2t  13724  mopnval  13873  isxms  13882  isms  13884  comet  13930  mopnex  13936  xmetxp  13938  xmetxpbl  13939  txmetcnp  13949  txmetcn  13950  qtopbasss  13952  cncfi  13996  cncfmpt1f  14015  ivthinclemlm  14043  ivthinclemum  14044  ivthinclemlopn  14045  ivthinclemlr  14046  ivthinclemuopn  14047  ivthinclemur  14048  ivthinclemdisj  14049  ivthinclemloc  14050  ivthinc  14052  ivthdec  14053  cnlimci  14073  limccnpcntop  14075  eldvap  14082  dvcoapbr  14102  dvcj  14104  dvfre  14105  dvmptcjx  14117  dveflem  14118  sin0pilem2  14134  pilem3  14135  coseq0q4123  14186  coseq0negpitopi  14188  cos11  14205  logltb  14226  rpcxpef  14246  rplogbval  14294  zabsle1  14331  lgslem2  14333  lgslem3  14334  lgsfcl2  14338  lgsfle1  14341  lgsle1  14347  lgsdirprm  14366  2sqlem1  14381  2sqlem2  14382  mul2sq  14383  2sqlem3  14384  2sqlem9  14391  2sqlem10  14392  012of  14665  2o01f  14666  subctctexmid  14670  nnsf  14674  nninfalllem1  14677  nninffeq  14689  qdencn  14695  trilpolemclim  14704  trilpolemcl  14705  trilpolemisumle  14706  trilpolemeq1  14708  trilpolemlt1  14709  trilpo  14711  iswomni0  14719  redcwlpo  14723  dceqnconst  14727  dcapnconst  14728  nconstwlpolemgt0  14731  nconstwlpolem  14732  nconstwlpo  14733  neapmkv  14735