Theorem fveq1i 3725

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

Syntax hints:   = wceq 956  ` cfv 3182

This theorem is referenced by:  fvopab3ig 3778  fvopab4gf 3781  fvopabgf 3787  fvopabnf 3788  fvsnun1 3795  fvsnun2 3796  elrnopabg 3800  fopab2 3823  rnssopab 3825  fopabco 3832  abrexexlem2 3859  dfrdg2 3933  rdgval 3940  rdgsucopab 3946  rdgsucopabn 3947  frsucopab 3954  abianfplem 3961  oprabval 4023  oprabvalig 4024  1stval 4081  2ndval 4082  curry1 4098  xpmapenlem5 4500  unblem2 4541  inf3lema 4609  inf3lemb 4610  inf3lemc 4611  trcl 4645  r10 4651  r1lim 4653  tz9.12lem3 4661  rankval 4668  ac6lem 4754  numthlem 4783  zorn2lem1 4788  oncardval 4819  cardval 4826  aleph0 4863  alephlim 4864  alephfplem1 4896  addpiord 5012  mulpiord 5013  om2uz0 6295  om2uzsuc 6296  seq1lem1 6309  seq1rval 6311  seq1suclem 6316  shftidt 6355  limsupvalt 6529  seq0valt 6536  seq1seq0t 6544  seq00 6550  seq0p1 6551  cbvsum 6986  sumeqfv 6997  fsumser0f 7001  fsumser1f 7002  serzfsum 7004  ser0clt 7046  ser1clt 7047  ser0mulc 7059  ser1mulc 7060  ser0cj 7065  iserzabslem 7178  isumval2t 7194  isumcmpi 7215  geosum 7241  efseq0ex 7311  effsumle 7397  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  ruclem10 7519  ruclem11 7520  cnmetdval 7902  remetdval 7908  qdensere2 7916  fsumcnlem 7989  vafval 8222  bafval 8223  smfval 8224  0vfval 8225  nmfval 8226  vsfval 8254  shftefif1olem 8741  eflogt 8760  logeft 8762  logeftb 8764  avril1 8784  pjoc2 9271  pjcj 9629  ho0valt 9676  hoivalt 9681  hhblo 9828  cnlnadjlem5 10004  adjbdlnb 10017  nmopcoadj 10034  hmopidmchlem 10078  hmopidmpj 10080  pjinvar 10119  pjadj2co 10132  pj3lem1 10134  symgval 10403  oprabvaligg 10440  fvopab2a 10463  trnij 10637  domval 10655  codval 10656  idval 10657  cmpval 10658  rdmob 10681  homib 10724  ismona 10737

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198

Copyright terms: Public domain