Theorem fveq2 5554

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 4032	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5237	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5262	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5262	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2251	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4029  ℩cio 5213  ‘cfv 5254

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  fveq2i  5557  fveq2d  5558  2fveq3  5559  fvifdc  5576  dffn5imf  5612  fvelimab  5613  ssimaex  5618  fvco4  5629  fvmptssdm  5642  fvmptf  5650  eqfnfv2f  5659  fvelrn  5689  ralrnmpt  5700  rexrnmpt  5701  ffnfvf  5717  fmptco  5724  cofmpt  5727  fcompt  5728  fcoconst  5729  fnressn  5744  fressnfv  5745  fconstfvm  5776  foco2  5796  funiunfvdmf  5807  f1veqaeq  5812  dff13f  5813  f1fveq  5815  f1elima  5816  f1ocnvfv  5822  f1ocnvfvb  5823  fcofo  5827  cocan2  5831  fliftfun  5839  isorel  5851  isocnv  5854  isotr  5859  f1oiso2  5870  canth  5871  imbrov2fvoveq  5943  ffnov  6022  eqfnov  6025  fnovim  6027  fnrnov  6064  foov  6065  funimassov  6068  ovelimab  6069  suppssfv  6126  ofvalg  6140  ofrval  6141  offval2  6146  ofrfval2  6147  ofco  6149  caofinvl  6155  op1std  6201  op2ndd  6202  1stval2  6208  2ndval2  6209  unielxp  6227  reldm  6239  oprabco  6270  2ndconst  6275  f1o2ndf1  6281  mpoxopn0yelv  6292  mpoxopoveq  6293  smoel  6353  tfrlem1  6361  tfrlem3-2d  6365  tfrlem5  6367  tfrlem9  6372  tfr0dm  6375  tfrlemiubacc  6383  tfrlemi1  6385  tfrexlem  6387  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemubacc  6399  tfr1onlemaccex  6401  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemubacc  6412  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  tfrcl  6417  tfri3  6420  rdgtfr  6427  rdgss  6436  rdgisuc1  6437  rdgisucinc  6438  rdgon  6439  frecabex  6451  frecabcl  6452  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  frecrdg  6461  oav  6507  omv  6508  oeiv  6509  fvixp  6757  cbvixp  6769  mptelixpg  6788  elixpsn  6789  dom2lem  6826  xpcomco  6880  xpmapen  6906  fidceq  6925  fieq0  7035  ordiso2  7094  djune  7137  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  omp1eom  7154  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumctlemm  7173  nninfninc  7182  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  finomni  7199  fodjuomnilemdc  7203  fodju0  7206  fodjuomni  7208  ismkvnex  7214  fodjumkv  7219  nninfwlporlemd  7231  nninfwlpor  7233  exmidaclem  7268  cc1  7325  cc2lem  7326  cc2  7327  cc3  7328  mulpipq2  7431  genipv  7569  genpelxp  7571  addcanprleml  7674  addcanprlemu  7675  recexprlemm  7684  recexprlemdisj  7690  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  cauappcvgprlemm  7705  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemnbj  7753  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgsrlemcl  7849  caucvgsrlemfv  7851  caucvgsrlembound  7854  caucvgsrlemgt1  7855  caucvgsrlemoffval  7856  caucvgsrlemoffres  7860  caucvgsrlembnd  7861  caucvgsr  7862  axcaucvglemcau  7958  axcaucvglemres  7959  uz11  9615  cnref1o  9716  fzprval  10148  fztpval  10149  frec2uzuzd  10473  frec2uzltd  10474  frec2uzlt2d  10475  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgtcl  10483  frecuzrdgg  10487  frecuzrdgfunlem  10490  frecfzennn  10497  seqeq1  10521  iseqovex  10529  seq3val  10531  seqvalcd  10532  seq3-1  10533  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3clss  10542  seq3fveq2  10546  seqfveq2g  10548  seqfveqg  10549  seq3fveq  10550  seq3feq  10551  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqval  10571  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1olemp  10586  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem2a  10589  seqf1og  10592  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  ser3le  10608  exp3vallem  10611  exp3val  10612  facp1  10801  faccl  10806  facdiv  10809  facwordi  10811  faclbnd  10812  facubnd  10816  bcval  10820  bcval5  10834  fz1eqb  10861  omgadd  10873  hashxp  10897  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  eqwrd  10954  seq3shft  10982  reval  10993  replim  11003  cj11  11049  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  rexuz3  11134  absval  11145  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  resqrexlemsqa  11168  resqrexlemex  11169  abs00bd  11210  cau3lem  11258  caubnd2  11261  climconst  11433  climmpt  11443  climshftlemg  11445  climcn1  11451  climle  11477  climub  11487  climserle  11488  climcau  11490  climcvg1nlem  11492  climcvg1n  11493  serf0  11495  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3  11530  fsumf1o  11533  fisumss  11535  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumadd  11549  sumsnf  11552  isummulc2  11569  isumge0  11573  isumadd  11574  fsum2dlemstep  11577  fsummulc2  11591  fsumconst  11597  fsumrelem  11614  isumshft  11633  isum1p  11635  isumnn0nn  11636  isumrpcl  11637  isumlessdc  11639  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2prod  11682  prodfap0  11688  prodfrecap  11689  prodfdivap  11690  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  prodsnf  11735  fprodfac  11758  fprodconst  11763  fprod2dlemstep  11765  eftvalcn  11800  ef0lem  11803  ege2le3  11814  efcj  11816  efaddlem  11817  eftlub  11833  efgt1p2  11838  reef11  11842  tanvalap  11851  efieq1re  11915  eirraplem  11920  dvdsabseq  11989  dvdsfac  12002  zsupcllemex  12083  infssuzex  12086  suprzubdc  12089  gcd0id  12116  nninfctlemfo  12177  nn0seqcvgd  12179  alginv  12185  algcvg  12186  algcvga  12189  algfx  12190  eucalglt  12195  lcmid  12218  qredeu  12235  prmfac1  12290  sqne2sq  12315  qnumdenbi  12330  dfphi2  12358  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  phisum  12378  pcmpt  12481  pcfac  12488  1arithlem4  12504  elgz  12509  4sqlem4  12530  4sqlem12  12540  ennnfonelemk  12557  ennnfonelemp1  12563  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemrn  12576  ennnfonelemnn0  12579  ennnfonelemr  12580  ennnfonelemim  12581  ctinfomlemom  12584  ctinfom  12585  ctiunctlemfo  12596  nninfdclemlt  12608  nninfdclemf1  12609  sloteq  12623  ressvalsets  12682  topnvalg  12862  imasex  12888  imasaddvallemg  12898  qusex  12908  xpsfrnel  12927  xpsfeq  12928  xpsval  12935  ismgm  12940  plusffvalg  12945  grpidvalg  12956  gsumfzval  12974  gsumval2  12980  issgrp  12986  ismnddef  12999  ismhm  13033  mhmex  13034  mhmlin  13039  issubm  13044  mhmeql  13064  isgrp  13078  grpn0  13107  grpinvfvalg  13114  grpsubfvalg  13117  grpsubval  13118  grpinv11  13141  grpinvnz  13143  mhmlem  13184  mulgfvalg  13191  mulgsubcl  13206  mulgaddcomlem  13215  mulgneg2  13226  mulgass  13229  issubg  13243  subgex  13246  issubg2m  13259  issubg4m  13263  0subg  13269  isnsg  13272  releqgg  13290  eqgex  13291  eqgval  13293  isghm  13313  ghmlin  13318  ghmrn  13327  ghmeql  13337  f1ghm0to0  13342  iscmn  13363  mgpvalg  13419  isrng  13430  issrg  13461  srgfcl  13469  isring  13496  iscrng  13499  mulgass2  13554  opprvalg  13565  reldvdsrsrg  13588  dvdsrvald  13589  isunitd  13602  invrfvald  13618  dvrfvald  13629  dvrvald  13630  isrhm  13654  rhmval  13669  isnzr  13677  islring  13688  issubrng  13695  issubrg  13717  rrgval  13758  isdomn  13765  aprval  13778  aprap  13782  islmod  13787  scaffvalg  13802  lsssetm  13852  lspfval  13884  sraval  13933  rlmvalg  13950  2idlval  13998  2idlvalg  13999  cnfldmulg  14064  zlmval  14115  znf1o  14139  istps  14200  clsfval  14269  cnpval  14366  lmconst  14384  txcnp  14439  upxp  14440  uptx  14442  txlm  14447  lmcn2  14448  cnmpt11  14451  cnmpt11f  14452  cnmpt1t  14453  cnmpt21  14459  cnmpt21f  14460  cnmpt2t  14461  mopnval  14610  isxms  14619  isms  14621  comet  14667  mopnex  14673  xmetxp  14675  xmetxpbl  14676  txmetcnp  14686  txmetcn  14687  qtopbasss  14689  cncfi  14733  cncfmpt1f  14752  ivthinclemlm  14788  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthdec  14798  ivthreinc  14799  cnlimci  14827  limccnpcntop  14829  eldvap  14836  dvcoapbr  14856  dvcj  14858  dvfre  14859  dvmptcjx  14871  dveflem  14872  elply2  14881  elplyd  14887  plymullem1  14894  plyadd  14897  plymul  14898  sin0pilem2  14917  pilem3  14918  coseq0q4123  14969  coseq0negpitopi  14971  cos11  14988  logltb  15009  rpcxpef  15029  rplogbval  15077  zabsle1  15115  lgslem2  15117  lgslem3  15118  lgsfcl2  15122  lgsfle1  15125  lgsle1  15131  lgsdirprm  15150  lgseisenlem2  15187  2sqlem1  15201  2sqlem2  15202  mul2sq  15203  2sqlem3  15204  2sqlem9  15211  2sqlem10  15212  012of  15486  2o01f  15487  subctctexmid  15491  nnsf  15495  nninfalllem1  15498  nninffeq  15510  qdencn  15517  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trilpo  15533  iswomni0  15541  redcwlpo  15545  dceqnconst  15550  dcapnconst  15551  nconstwlpolemgt0  15554  nconstwlpolem  15555  nconstwlpo  15556  neapmkv  15558