Theorem fveq2 5375

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 3898	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝑥 ↔ 𝐵𝐹𝑥))
2	1	iotabidv 5067	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3		df-fv 5089	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5089	. 2 ⊢ (𝐹‘𝐵) = (℩𝑥𝐵𝐹𝑥)
5	2, 3, 4	3eqtr4g 2172	1 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1314   class class class wbr 3895  ℩cio 5044  ‘cfv 5081

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-rex 2396  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-iota 5046  df-fv 5089

This theorem is referenced by:  fveq2i  5378  fveq2d  5379  2fveq3  5380  fvifdc  5397  dffn5imf  5430  fvelimab  5431  ssimaex  5436  fvco4  5447  fvmptssdm  5459  fvmptf  5467  eqfnfv2f  5476  fvelrn  5505  ralrnmpt  5516  rexrnmpt  5517  ffnfvf  5533  fmptco  5540  cofmpt  5543  fcompt  5544  fcoconst  5545  fnressn  5560  fressnfv  5561  fconstfvm  5592  foco2  5609  funiunfvdmf  5619  f1veqaeq  5624  dff13f  5625  f1fveq  5627  f1elima  5628  f1ocnvfv  5634  f1ocnvfvb  5635  fcofo  5639  cocan2  5643  fliftfun  5651  isorel  5663  isocnv  5666  isotr  5671  f1oiso2  5682  imbrov2fvoveq  5753  ffnov  5829  eqfnov  5831  fnovim  5833  fnrnov  5870  foov  5871  funimassov  5874  ovelimab  5875  suppssfv  5932  ofvalg  5945  ofrval  5946  offval2  5951  ofrfval2  5952  ofco  5954  caofinvl  5958  op1std  6000  op2ndd  6001  1stval2  6007  2ndval2  6008  unielxp  6026  reldm  6038  oprabco  6068  2ndconst  6073  f1o2ndf1  6079  mpoxopn0yelv  6090  mpoxopoveq  6091  smoel  6151  tfrlem1  6159  tfrlem3-2d  6163  tfrlem5  6165  tfrlem9  6170  tfr0dm  6173  tfrlemiubacc  6181  tfrlemi1  6183  tfrexlem  6185  tfr1onlemsucfn  6191  tfr1onlemsucaccv  6192  tfr1onlembxssdm  6194  tfr1onlembfn  6195  tfr1onlemubacc  6197  tfr1onlemaccex  6199  tfr1onlemres  6200  tfri1dALT  6202  tfrcllemsucfn  6204  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllembfn  6208  tfrcllemubacc  6210  tfrcllemaccex  6212  tfrcllemres  6213  tfrcldm  6214  tfrcl  6215  tfri3  6218  rdgtfr  6225  rdgss  6234  rdgisuc1  6235  rdgisucinc  6236  rdgon  6237  frecabex  6249  frecabcl  6250  frecfcllem  6255  frecsuclem  6257  frecsuc  6258  frecrdg  6259  oav  6304  omv  6305  oeiv  6306  fvixp  6551  cbvixp  6563  mptelixpg  6582  elixpsn  6583  dom2lem  6620  xpcomco  6673  xpmapen  6697  fidceq  6716  fieq0  6816  ordiso2  6872  djune  6915  updjudhcoinlf  6917  updjudhcoinrg  6918  updjud  6919  omp1eom  6932  0ct  6944  ctmlemr  6945  ctssdclemn0  6947  ctssdccl  6948  ctssdc  6950  enumctlemm  6951  enomnilem  6960  finomni  6962  fodjuomnilemdc  6966  fodju0  6969  fodjuomni  6971  ismkvnex  6979  fodjumkv  6984  exmidaclem  7012  mulpipq2  7124  genipv  7262  genpelxp  7264  addcanprleml  7367  addcanprlemu  7368  recexprlemm  7377  recexprlemdisj  7383  recexprlemloc  7384  recexprlem1ssl  7386  recexprlem1ssu  7387  cauappcvgprlemm  7398  cauappcvgprlemdisj  7404  cauappcvgprlemloc  7405  cauappcvgprlemladdru  7409  cauappcvgprlemladdrl  7410  cauappcvgprlem1  7412  cauappcvgprlem2  7413  cauappcvgprlemlim  7414  cauappcvgpr  7415  caucvgprlemnkj  7419  caucvgprlemnbj  7420  caucvgprlemm  7421  caucvgprlemdisj  7427  caucvgprlemloc  7428  caucvgprlemcl  7429  caucvgprlemladdfu  7430  caucvgprlemladdrl  7431  caucvgprlem1  7432  caucvgprlem2  7433  caucvgpr  7435  caucvgprprlemell  7438  caucvgprprlemelu  7439  caucvgprprlemcbv  7440  caucvgprprlemval  7441  caucvgprprlemnkeqj  7443  caucvgprprlemnbj  7446  caucvgprprlemml  7447  caucvgprprlemmu  7448  caucvgprprlemopl  7450  caucvgprprlemlol  7451  caucvgprprlemopu  7452  caucvgprprlemloc  7456  caucvgprprlemclphr  7458  caucvgprprlemexbt  7459  caucvgprprlem1  7462  caucvgprprlem2  7463  caucvgsrlemcl  7528  caucvgsrlemfv  7530  caucvgsrlembound  7533  caucvgsrlemgt1  7534  caucvgsrlemoffval  7535  caucvgsrlemoffres  7539  caucvgsrlembnd  7540  caucvgsr  7541  axcaucvglemcau  7630  axcaucvglemres  7631  uz11  9247  cnref1o  9339  fzprval  9752  fztpval  9753  frec2uzuzd  10065  frec2uzltd  10066  frec2uzlt2d  10067  frecuzrdgrrn  10071  frec2uzrdg  10072  frecuzrdgtcl  10075  frecuzrdgg  10079  frecuzrdgfunlem  10082  frecfzennn  10089  seqeq1  10111  iseqovex  10119  seq3val  10121  seqvalcd  10122  seq3-1  10123  seqf  10124  seq3p1  10125  seqovcd  10126  seqp1cd  10129  seq3clss  10130  seq3fveq2  10132  seq3fveq  10134  seq3feq  10135  seq3shft2  10136  monoord  10139  monoord2  10140  ser3mono  10141  seq3split  10142  seq3caopr3  10144  seq3caopr2  10145  iseqf1olemkle  10147  iseqf1olemklt  10148  iseqf1olemqval  10150  iseqf1olemqk  10157  iseqf1olemjpcl  10158  iseqf1olemqpcl  10159  iseqf1olemfvp  10160  seq3f1olemqsumkj  10161  seq3f1olemqsum  10163  seq3f1olemstep  10164  seq3f1olemp  10165  seq3f1oleml  10166  seq3f1o  10167  seq3id2  10172  seq3homo  10173  seq3z  10174  ser3ge0  10180  ser3le  10181  exp3vallem  10184  exp3val  10185  facp1  10366  faccl  10371  facdiv  10374  facwordi  10376  faclbnd  10377  facubnd  10381  bcval  10385  bcval5  10399  fz1eqb  10427  omgadd  10438  hashxp  10462  zfz1isolem1  10473  zfz1iso  10474  seq3coll  10475  seq3shft  10500  reval  10511  replim  10521  cj11  10567  caucvgre  10642  cvg1nlemcau  10645  cvg1nlemres  10646  rexuz3  10651  absval  10662  resqrexlemover  10671  resqrexlemdecn  10673  resqrexlemlo  10674  resqrexlemcalc3  10677  resqrexlemnm  10679  resqrexlemcvg  10680  resqrexlemoverl  10682  resqrexlemglsq  10683  resqrexlemga  10684  resqrexlemsqa  10685  resqrexlemex  10686  abs00bd  10727  cau3lem  10775  caubnd2  10778  climconst  10948  climmpt  10958  climshftlemg  10960  climcn1  10966  climle  10992  climub  11002  climserle  11003  climcau  11005  climcvg1nlem  11007  climcvg1n  11008  serf0  11010  fsum3cvg  11035  summodclem3  11038  summodclem2a  11039  summodclem2  11040  summodc  11041  zsumdc  11042  fsum3  11045  fsumf1o  11048  fisumss  11050  fsum3cvg2  11052  fsum3ser  11055  fsumcl2lem  11056  fsumadd  11064  sumsnf  11067  isummulc2  11084  isumge0  11088  isumadd  11089  fsum2dlemstep  11092  fsummulc2  11106  fsumconst  11112  fsumrelem  11129  isumshft  11148  isum1p  11150  isumnn0nn  11151  isumrpcl  11152  isumlessdc  11154  cvgratnnlemnexp  11182  cvgratnnlemmn  11183  cvgratnnlemseq  11184  cvgratnnlemabsle  11185  cvgratnnlemfm  11187  cvgratnnlemrate  11188  cvgratnn  11189  cvgratz  11190  mertenslemi1  11193  mertenslem2  11194  mertensabs  11195  eftvalcn  11211  ef0lem  11214  ege2le3  11225  efcj  11227  efaddlem  11228  eftlub  11244  efgt1p2  11249  reef11  11254  tanvalap  11263  efieq1re  11325  eirraplem  11328  dvdsabseq  11390  dvdsfac  11403  zsupcllemex  11484  infssuzex  11487  gcd0id  11512  nn0seqcvgd  11565  alginv  11571  algcvg  11572  algcvga  11575  algfx  11576  eucalglt  11581  lcmid  11604  qredeu  11621  prmfac1  11673  sqne2sq  11697  qnumdenbi  11712  dfphi2  11738  ennnfonelemk  11755  ennnfonelemp1  11761  ennnfoneleminc  11766  ennnfonelemkh  11767  ennnfonelemhf1o  11768  ennnfonelemex  11769  ennnfonelemhom  11770  ennnfonelemrn  11774  ennnfonelemnn0  11777  ennnfonelemr  11778  ennnfonelemim  11779  ctinfomlemom  11782  ctinfom  11783  ctiunctlemfo  11792  sloteq  11804  topnvalg  11972  istps  12039  clsfval  12110  cnpval  12206  lmconst  12224  txcnp  12279  upxp  12280  uptx  12282  txlm  12287  lmcn2  12288  cnmpt11  12291  cnmpt11f  12292  cnmpt1t  12293  cnmpt21  12299  cnmpt21f  12300  cnmpt2t  12301  mopnval  12428  isxms  12437  isms  12439  comet  12485  mopnex  12491  xmetxp  12493  xmetxpbl  12494  txmetcnp  12504  txmetcn  12505  qtopbasss  12507  cncfi  12548  cncfmpt1f  12567  cnlimci  12595  limccnpcntop  12597  eldvap  12603  subctctexmid  12880  nnsf  12883  nninfalllemn  12886  nninfalllem1  12887  nninfomnilem  12898  nninffeq  12900  qdencn  12906  isomninnlem  12909  trilpolemclim  12913  trilpolemcl  12914  trilpolemisumle  12915  trilpolemeq1  12917  trilpolemlt1  12918  trilpo  12920