Theorem fveq2 5594

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 4057	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5268	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5293	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5293	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2264	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4054  ℩cio 5244  ‘cfv 5285

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-iota 5246  df-fv 5293

This theorem is referenced by:  fveq2i  5597  fveq2d  5598  2fveq3  5599  fvifdc  5616  dffn5imf  5652  fvelimab  5653  ssimaex  5658  fvco4  5669  fvmptssdm  5682  fvmptf  5690  eqfnfv2f  5699  fvelrn  5729  ralrnmpt  5740  rexrnmpt  5741  ffnfvf  5757  fmptco  5764  cofmpt  5767  fcompt  5768  fcoconst  5769  fnressn  5788  fressnfv  5789  fconstfvm  5820  foco2  5840  funiunfvdmf  5851  f1veqaeq  5856  dff13f  5857  f1fveq  5859  f1elima  5860  f1ocnvfv  5866  f1ocnvfvb  5867  fcofo  5871  cocan2  5875  fliftfun  5883  isorel  5895  isocnv  5898  isotr  5903  f1oiso2  5914  canth  5915  imbrov2fvoveq  5987  ffnov  6067  eqfnov  6070  fnovim  6072  fnrnov  6110  foov  6111  funimassov  6114  ovelimab  6115  suppssfv  6172  ofvalg  6186  ofrval  6187  offval2  6192  ofrfval2  6193  ofco  6195  caofinvl  6202  op1std  6252  op2ndd  6253  1stval2  6259  2ndval2  6260  unielxp  6278  reldm  6290  oprabco  6321  2ndconst  6326  f1o2ndf1  6332  mpoxopn0yelv  6343  mpoxopoveq  6344  smoel  6404  tfrlem1  6412  tfrlem3-2d  6416  tfrlem5  6418  tfrlem9  6423  tfr0dm  6426  tfrlemiubacc  6434  tfrlemi1  6436  tfrexlem  6438  tfr1onlemsucfn  6444  tfr1onlemsucaccv  6445  tfr1onlembxssdm  6447  tfr1onlembfn  6448  tfr1onlemubacc  6450  tfr1onlemaccex  6452  tfr1onlemres  6453  tfri1dALT  6455  tfrcllemsucfn  6457  tfrcllemsucaccv  6458  tfrcllembxssdm  6460  tfrcllembfn  6461  tfrcllemubacc  6463  tfrcllemaccex  6465  tfrcllemres  6466  tfrcldm  6467  tfrcl  6468  tfri3  6471  rdgtfr  6478  rdgss  6487  rdgisuc1  6488  rdgisucinc  6489  rdgon  6490  frecabex  6502  frecabcl  6503  frecfcllem  6508  frecsuclem  6510  frecsuc  6511  frecrdg  6512  oav  6558  omv  6559  oeiv  6560  fvixp  6808  cbvixp  6820  mptelixpg  6839  elixpsn  6840  dom2lem  6881  xpcomco  6941  xpmapen  6967  fidceq  6987  fieq0  7099  ordiso2  7158  djune  7201  updjudhcoinlf  7203  updjudhcoinrg  7204  updjud  7205  omp1eom  7218  0ct  7230  ctmlemr  7231  ctssdclemn0  7233  ctssdccl  7234  ctssdc  7236  enumctlemm  7237  nninfninc  7246  nnnninfeq  7251  nnnninfeq2  7252  enomnilem  7261  finomni  7263  fodjuomnilemdc  7267  fodju0  7270  fodjuomni  7272  ismkvnex  7278  fodjumkv  7283  nninfwlporlemd  7295  nninfwlpor  7297  exmidaclem  7346  cc1  7407  cc2lem  7408  cc2  7409  cc3  7410  mulpipq2  7514  genipv  7652  genpelxp  7654  addcanprleml  7757  addcanprlemu  7758  recexprlemm  7767  recexprlemdisj  7773  recexprlemloc  7774  recexprlem1ssl  7776  recexprlem1ssu  7777  cauappcvgprlemm  7788  cauappcvgprlemdisj  7794  cauappcvgprlemloc  7795  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  cauappcvgprlem1  7802  cauappcvgprlem2  7803  cauappcvgprlemlim  7804  cauappcvgpr  7805  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprlemm  7811  caucvgprlemdisj  7817  caucvgprlemloc  7818  caucvgprlemcl  7819  caucvgprlemladdfu  7820  caucvgprlemladdrl  7821  caucvgprlem1  7822  caucvgprlem2  7823  caucvgpr  7825  caucvgprprlemell  7828  caucvgprprlemelu  7829  caucvgprprlemcbv  7830  caucvgprprlemval  7831  caucvgprprlemnkeqj  7833  caucvgprprlemnbj  7836  caucvgprprlemml  7837  caucvgprprlemmu  7838  caucvgprprlemopl  7840  caucvgprprlemlol  7841  caucvgprprlemopu  7842  caucvgprprlemloc  7846  caucvgprprlemclphr  7848  caucvgprprlemexbt  7849  caucvgprprlem1  7852  caucvgprprlem2  7853  caucvgsrlemcl  7932  caucvgsrlemfv  7934  caucvgsrlembound  7937  caucvgsrlemgt1  7938  caucvgsrlemoffval  7939  caucvgsrlemoffres  7943  caucvgsrlembnd  7944  caucvgsr  7945  axcaucvglemcau  8041  axcaucvglemres  8042  uz11  9701  cnref1o  9802  fzprval  10234  fztpval  10235  zsupcllemex  10405  infssuzex  10408  suprzubdc  10411  frec2uzuzd  10579  frec2uzltd  10580  frec2uzlt2d  10581  frecuzrdgrrn  10585  frec2uzrdg  10586  frecuzrdgtcl  10589  frecuzrdgg  10593  frecuzrdgfunlem  10596  frecfzennn  10603  seqeq1  10627  iseqovex  10635  seq3val  10637  seqvalcd  10638  seq3-1  10639  seqf  10641  seq3p1  10642  seqovcd  10644  seqp1cd  10647  seq3clss  10648  seq3fveq2  10652  seqfveq2g  10654  seqfveqg  10655  seq3fveq  10656  seq3feq  10657  seq3shft2  10658  seqshft2g  10659  monoord  10662  monoord2  10663  ser3mono  10664  seq3split  10665  seqsplitg  10666  seq3caopr3  10668  seqcaopr3g  10669  seq3caopr2  10670  seqcaopr2g  10671  iseqf1olemkle  10674  iseqf1olemklt  10675  iseqf1olemqval  10677  iseqf1olemqk  10684  iseqf1olemjpcl  10685  iseqf1olemqpcl  10686  iseqf1olemfvp  10687  seq3f1olemqsumkj  10688  seq3f1olemqsum  10690  seq3f1olemstep  10691  seq3f1olemp  10692  seq3f1oleml  10693  seq3f1o  10694  seqf1oglem2a  10695  seqf1og  10698  seq3id2  10703  seq3homo  10704  seq3z  10705  seqhomog  10707  seqfeq4g  10708  ser3ge0  10713  ser3le  10714  exp3vallem  10717  exp3val  10718  facp1  10907  faccl  10912  facdiv  10915  facwordi  10917  faclbnd  10918  facubnd  10922  bcval  10926  bcval5  10940  fz1eqb  10967  omgadd  10979  hashxp  11003  zfz1isolem1  11017  zfz1iso  11018  seq3coll  11019  eqwrd  11066  lswwrd  11072  lswex  11077  ccatfvalfi  11081  ccatval1  11086  ccatval2  11087  s1eq  11106  eqs1  11115  swrdval  11134  ccatopth2  11203  wrd2ind  11209  seq3shft  11234  reval  11245  replim  11255  cj11  11301  caucvgre  11377  cvg1nlemcau  11380  cvg1nlemres  11381  rexuz3  11386  absval  11397  resqrexlemover  11406  resqrexlemdecn  11408  resqrexlemlo  11409  resqrexlemcalc3  11412  resqrexlemnm  11414  resqrexlemcvg  11415  resqrexlemoverl  11417  resqrexlemglsq  11418  resqrexlemga  11419  resqrexlemsqa  11420  resqrexlemex  11421  abs00bd  11462  cau3lem  11510  caubnd2  11513  climconst  11686  climmpt  11696  climshftlemg  11698  climcn1  11704  climle  11730  climub  11740  climserle  11741  climcau  11743  climcvg1nlem  11745  climcvg1n  11746  serf0  11748  fsum3cvg  11774  summodclem3  11776  summodclem2a  11777  summodclem2  11778  summodc  11779  zsumdc  11780  fsum3  11783  fsumf1o  11786  fisumss  11788  fsum3cvg2  11790  fsum3ser  11793  fsumcl2lem  11794  fsumadd  11802  sumsnf  11805  isummulc2  11822  isumge0  11826  isumadd  11827  fsum2dlemstep  11830  fsummulc2  11844  fsumconst  11850  fsumrelem  11867  isumshft  11886  isum1p  11888  isumnn0nn  11889  isumrpcl  11890  isumlessdc  11892  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  cvgratnnlemseq  11922  cvgratnnlemabsle  11923  cvgratnnlemfm  11925  cvgratnnlemrate  11926  cvgratnn  11927  cvgratz  11928  mertenslemi1  11931  mertenslem2  11932  mertensabs  11933  clim2prod  11935  prodfap0  11941  prodfrecap  11942  prodfdivap  11943  fproddccvg  11968  prodmodclem3  11971  prodmodclem2a  11972  prodmodclem2  11973  prodmodc  11974  zproddc  11975  fprodseq  11979  fprodf1o  11984  fprodssdc  11986  fprodmul  11987  prodsnf  11988  fprodfac  12011  fprodconst  12016  fprod2dlemstep  12018  eftvalcn  12053  ef0lem  12056  ege2le3  12067  efcj  12069  efaddlem  12070  eftlub  12086  efgt1p2  12091  reef11  12095  tanvalap  12104  efieq1re  12168  eirraplem  12173  dvdsabseq  12243  dvdsfac  12256  gcd0id  12385  nninfctlemfo  12446  nn0seqcvgd  12448  alginv  12454  algcvg  12455  algcvga  12458  algfx  12459  eucalglt  12464  lcmid  12487  qredeu  12504  prmfac1  12559  sqne2sq  12584  qnumdenbi  12599  dfphi2  12627  eulerthlemrprm  12636  eulerthlema  12637  eulerthlemh  12638  eulerthlemth  12639  phisum  12648  pcmpt  12751  pcfac  12758  1arithlem4  12774  elgz  12779  4sqlem4  12800  4sqlem12  12810  2expltfac  12847  ennnfonelemk  12856  ennnfonelemp1  12862  ennnfoneleminc  12867  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemex  12870  ennnfonelemhom  12871  ennnfonelemrn  12875  ennnfonelemnn0  12878  ennnfonelemr  12879  ennnfonelemim  12880  ctinfomlemom  12883  ctinfom  12884  ctiunctlemfo  12895  nninfdclemlt  12907  nninfdclemf1  12908  sloteq  12922  ressvalsets  12981  topnvalg  13168  prdsbasprj  13199  prdsplusgfval  13201  prdsmulrfval  13203  imasex  13222  imasaddvallemg  13232  qusex  13242  xpsfrnel  13261  xpsfeq  13262  xpsval  13269  ismgm  13274  plusffvalg  13279  grpidvalg  13290  gsumfzval  13308  gsumval2  13314  issgrp  13320  ismnddef  13335  prdsidlem  13364  pws0g  13368  ismhm  13378  mhmex  13379  mhmlin  13384  issubm  13389  mhmeql  13409  isgrp  13423  grpn0  13452  grpinvfvalg  13459  grpsubfvalg  13462  grpsubval  13463  grpinv11  13486  grpinvnz  13488  prdsinvlem  13525  pwsinvg  13529  pwssub  13530  mhmlem  13535  mulgfvalg  13542  mulgsubcl  13557  mulgaddcomlem  13566  mulgneg2  13577  mulgass  13580  issubg  13594  subgex  13597  issubg2m  13610  issubg4m  13614  0subg  13620  isnsg  13623  releqgg  13641  eqgex  13642  eqgval  13644  isghm  13664  ghmlin  13669  ghmrn  13678  ghmeql  13688  f1ghm0to0  13693  iscmn  13714  mgpvalg  13770  isrng  13781  issrg  13812  srgfcl  13820  isring  13847  iscrng  13850  mulgass2  13905  opprvalg  13916  reldvdsrsrg  13939  dvdsrvald  13940  isunitd  13953  invrfvald  13969  dvrfvald  13980  dvrvald  13981  isrhm  14005  rhmval  14020  isnzr  14028  islring  14039  issubrng  14046  issubrg  14068  rrgval  14109  isdomn  14116  aprval  14129  aprap  14133  islmod  14138  scaffvalg  14153  lsssetm  14203  lspfval  14235  sraval  14284  rlmvalg  14301  2idlval  14349  2idlvalg  14350  cnfldmulg  14423  zlmval  14474  znf1o  14498  psrlinv  14531  mplsubgfilemcl  14546  istps  14589  clsfval  14658  cnpval  14755  lmconst  14773  txcnp  14828  upxp  14829  uptx  14831  txlm  14836  lmcn2  14837  cnmpt11  14840  cnmpt11f  14841  cnmpt1t  14842  cnmpt21  14848  cnmpt21f  14849  cnmpt2t  14850  mopnval  14999  isxms  15008  isms  15010  comet  15056  mopnex  15062  xmetxp  15064  xmetxpbl  15065  txmetcnp  15075  txmetcn  15076  qtopbasss  15078  cncfi  15135  cncfmpt1f  15155  ivthinclemlm  15191  ivthinclemum  15192  ivthinclemlopn  15193  ivthinclemlr  15194  ivthinclemuopn  15195  ivthinclemur  15196  ivthinclemdisj  15197  ivthinclemloc  15198  ivthinc  15200  ivthdec  15201  ivthreinc  15202  cnlimci  15230  limccnpcntop  15232  eldvap  15239  dvcoapbr  15264  dvcj  15266  dvfre  15267  dvmptcjx  15281  dveflem  15283  elply2  15292  elplyd  15298  plymullem1  15305  plyadd  15308  plymul  15309  plycoeid3  15314  plycolemc  15315  plyco  15316  plycjlemc  15317  plycj  15318  dvply1  15322  sin0pilem2  15339  pilem3  15340  coseq0q4123  15391  coseq0negpitopi  15393  cos11  15410  logltb  15431  rpcxpef  15451  rplogbval  15502  mpodvdsmulf1o  15547  fsumdvdsmul  15548  zabsle1  15561  lgslem2  15563  lgslem3  15564  lgsfcl2  15568  lgsfle1  15571  lgsle1  15577  lgsdirprm  15596  lgseisenlem2  15633  lgsquadlem2  15640  2sqlem1  15676  2sqlem2  15677  mul2sq  15678  2sqlem3  15679  2sqlem9  15686  2sqlem10  15687  vtxvalg  15700  iedgvalg  15701  edgvalg  15741  edgopval  15743  edgstruct  15745  isuhgrm  15752  isushgrm  15753  isupgren  15776  isumgren  15786  012of  16100  2o01f  16101  subctctexmid  16109  nnsf  16114  nninfalllem1  16117  nninffeq  16129  qdencn  16138  trilpolemclim  16147  trilpolemcl  16148  trilpolemisumle  16149  trilpolemeq1  16151  trilpolemlt1  16152  trilpo  16154  iswomni0  16162  redcwlpo  16166  dceqnconst  16171  dcapnconst  16172  nconstwlpolemgt0  16175  nconstwlpolem  16176  nconstwlpo  16177  neapmkv  16179