Theorem fveq1i 3732

Description: Equality inference for function value.

Hypothesis

Ref	Expression
fveq1i.1	|- F = G

Assertion

Ref	Expression
fveq1i	|- (F` A) = (G` A)

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 |- F = G
2		fveq1 3730	. 2 |- (F = G -> (F` A) = (G` A))
3	1, 2	ax-mp 7	1 |- (F` A) = (G` A)

Syntax hints:   = wceq 958  ` cfv 3189

This theorem is referenced by:  fvopab3ig 3785  fvopab4gf 3788  fvopabgf 3794  fvopabnf 3795  fvsnun1 3802  fvsnun2 3803  elrnopabg 3807  fopab2 3830  rnssopab 3832  fopabco 3839  abrexexlem2 3866  dfrdg2 3940  rdgval 3947  rdgsucopab 3953  rdgsucopabn 3954  frsucopab 3961  abianfplem 3968  oprabval 4030  oprabvalig 4031  1stval 4088  2ndval 4089  curry1 4105  xpmapenlem5 4507  unblem2 4554  inf3lema 4625  inf3lemb 4626  inf3lemc 4627  trcl 4662  r10 4668  r1lim 4670  tz9.12lem3 4678  rankval 4685  ac6lem 4771  numthlem 4800  zorn2lem1 4805  oncardval 4836  cardval 4843  aleph0 4881  alephlim 4882  alephfplem1 4914  addpiord 5031  mulpiord 5032  om2uz0 6303  om2uzsuc 6304  seq1lem1 6317  seq1rval 6319  seq1suclem 6324  shftidt 6363  limsupvalt 6537  seq0valt 6544  seq1seq0t 6552  seq00 6558  seq0p1 6559  cbvsum 6993  sumeqfv 7004  fsumser0f 7008  fsumser1f 7009  serzfsum 7011  ser0clt 7053  ser1clt 7054  ser0mulc 7066  ser1mulc 7067  ser0cj 7072  iserzabslem 7185  isumval2t 7201  isumcmpi 7222  geosum 7248  efseq0ex 7318  effsumle 7404  acdc3lem 7494  acdc2lem2 7497  acdc5lem2 7500  acdclem 7502  ruclem10 7527  ruclem11 7528  cnmetdval 7906  remetdval 7912  qdensere2 7920  fsumcnlem 7993  vafval 8225  bafval 8226  smfval 8227  0vfval 8228  nmfval 8229  vsfval 8257  shftefif1olem 8743  eflogt 8762  logeft 8764  logeftb 8766  avril1 8786  pjoc2 9273  pjcj 9631  ho0valt 9678  hoivalt 9683  hhblo 9830  cnlnadjlem5 10006  adjbdlnb 10019  nmopcoadj 10036  hmopidmchlem 10080  hmopidmpj 10082  pjinvar 10122  pjadj2co 10135  pj3lem1 10137  symgval 10406  oprabvaligg 10443  fvopab2a 10461  trnij 10616  domval 10634  codval 10635  idval 10636  cmpval 10637  rdmob 10660  homib 10703  ismona 10716

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-cnv 3193  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fv 3205

Copyright terms: Public domain