Theorem fveq1i 3836

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

Syntax hints:   = wceq 992  ` cfv 3263

This theorem is referenced by:  fvopab3ig 3889  fvopab4gf 3892  fvopabgf 3898  fvopabnf 3899  fvsnun1 3907  fvsnun2 3908  elrnopabg 3914  fopab2 3937  rnssopab 3939  fopabco 3946  abrexexlem2 3973  oprabval 4083  oprabvalig 4084  1stval 4142  2ndval 4143  curry1 4193  curry2 4196  dfrdg2 4234  rdgval 4241  rdgsucopab 4247  rdgsucopabn 4248  frsucopab 4255  abianfplem 4262  xpmapenlem5 4647  unblem2 4687  inf3lema 4754  inf3lemb 4755  inf3lemc 4756  trcl 4791  r10 4797  r1lim 4799  tz9.12lem3 4807  rankval 4814  ac6lem 4900  numthlem 4929  zorn2lem1 4934  oncardval 4965  cardval 4973  aleph0 5013  alephlim 5014  alephfplem1 5046  addpiord 5166  mulpiord 5167  om2uz0i 6658  om2uzsuci 6659  seq1lem1 6674  seq1rval 6676  seq1suclem 6681  shftidt 6720  limsupval 6724  seq0valt 6731  seq1seq01 6739  seq00 6745  seq0p1 6746  cbvsumi 7189  sumeqfv 7200  fsumser0fi 7204  fsumser1fi 7205  serzfsum 7207  ser0cl 7249  ser1cl 7250  ser0mulci 7262  ser1mulci 7263  ser0cji 7268  iserzabslem 7381  isumval2 7398  isumcmpii 7419  geosumi 7446  efseq0ex 7516  effsumlei 7605  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  ruclem10 7731  ruclem11 7732  cnmetdval 8113  remetdval 8119  qdensere2 8127  fsumcnlem 8200  gid0 8271  grpidval 8275  vafval 8469  bafval 8470  smfval 8471  0vfval 8472  nmfval 8473  vsfval 8501  vacnlem6 8587  shftefif1olem 9013  eflog 9032  logef 9034  logeftb 9036  avril1 9058  pjoc2i 9547  pjcji 9907  ho0val 9956  hoival 9961  hhbloi 10108  cnlnadjlem5 10283  adjbdlnb 10296  nmopcoadji 10313  hmopidmchlem 10358  hmopidmpji 10360  pjinvari 10400  pjadj2coi 10413  pj3lem1 10415  symgval 10688  oprabvaligg 10729  fvopab2a 10747  expmiz 10936  expm 10937  trnij 11160  domval 11177  codval 11178  idval 11179  cmpval 11180  rdmob 11202  homib 11251  ismona 11264  issubcat 11299  fictblem 11422  fictb 11423  ordtypelem1 11427  ordtypelem6 11432  omsubsuc 11438  subcls 11481  subntr 11482  neibastop2lem4 11583  fgf 11632  sfcls 11716  tailf 11756  upxp 11822  fsumleisumi 11889  piececn 11955  bfplem2 12055  bfplem3 12056

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279

Copyright terms: Public domain