Theorem fveq1i 3720

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 3718	. 2 |- (F = G -> (F` A) = (G` A))
3	1, 2	ax-mp 7	1 |- (F` A) = (G` A)

Syntax hints:   = wceq 955  ` cfv 3178

This theorem is referenced by:  fvopab3ig 3773  fvopab4gf 3776  fvopabgf 3782  fvopabnf 3783  fvsnun1 3790  fvsnun2 3791  elrnopabg 3795  fopab2 3818  rnssopab 3820  fopabco 3827  abrexexlem2 3854  dfrdg2 3928  rdgval 3935  rdgsucopab 3941  rdgsucopabn 3942  frsucopab 3949  abianfplem 3956  oprabval 4018  oprabvalig 4019  1stval 4074  2ndval 4075  curry1 4091  xpmapenlem5 4489  unblem2 4527  inf3lema 4592  inf3lemb 4593  inf3lemc 4594  trcl 4628  r10 4634  r1lim 4636  tz9.12lem3 4644  rankval 4651  ac6lem 4737  numthlem 4766  zorn2lem1 4771  oncardval 4802  cardval 4809  aleph0 4846  alephlim 4847  alephfplem1 4879  addpiord 4995  mulpiord 4996  om2uz0 6245  om2uzsuc 6246  seq1lem1 6259  seq1rval 6261  seq1suclem 6266  shftidt 6305  limsupvalt 6474  seq0valt 6481  seq1seq0t 6489  seq00 6495  seq0p1 6496  cbvsum 6939  sumeqfv 6950  fsumser0f 6954  fsumser1f 6955  serzfsum 6957  ser0clt 6999  ser1clt 7000  ser0mulc 7012  ser1mulc 7013  ser0cj 7018  iserzabslem 7131  isumval2t 7147  isumcmpi 7167  geosum 7193  efseq0ex 7270  effsumle 7355  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  ruclem10 7479  ruclem11 7480  cnmetdval 7864  remetdval 7870  qdensere2 7878  fsumcnlem 7951  vafval 8186  bafval 8187  smfval 8188  0vfval 8189  nmfval 8190  vsfval 8218  shftefif1olem 8696  eflogt 8715  logeft 8717  logeftb 8719  avril1 8739  pjoc2 9226  pjcj 9586  ho0valt 9633  hoivalt 9638  hhblo 9785  cnlnadjlem5 9960  adjbdlnb 9973  nmopcoadj 9990  hmopidmchlem 10034  hmopidmpj 10036  pjinvar 10075  pjadj2co 10088  pj3lem1 10090  symgval 10359  oprabvaligg 10399  fvopab2a 10417  trnij 10553  domval 10571  codval 10572  idval 10573  cmpval 10574  rdmob 10597  homib 10640  ismona 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-cnv 3182  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fv 3194

Copyright terms: Public domain