Theorem fveq1i 3801

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

Syntax hints:   = wceq 988  ` cfv 3237

This theorem is referenced by:  fvopab3ig 3854  fvopab4gf 3857  fvopabgf 3863  fvopabnf 3864  fvsnun1 3871  fvsnun2 3872  elrnopabg 3876  fopab2 3899  rnssopab 3901  fopabco 3908  abrexexlem2 3935  dfrdg2 4009  rdgval 4016  rdgsucopab 4022  rdgsucopabn 4023  frsucopab 4030  abianfplem 4037  oprabval 4100  oprabvalig 4101  1stval 4159  2ndval 4160  curry1 4208  curry2 4211  xpmapenlem5 4589  unblem2 4628  inf3lema 4695  inf3lemb 4696  inf3lemc 4697  trcl 4731  r10 4737  r1lim 4739  tz9.12lem3 4747  rankval 4754  ac6lem 4840  numthlem 4869  zorn2lem1 4874  oncardval 4905  cardval 4913  aleph0 4952  alephlim 4953  alephfplem1 4985  addpiord 5101  mulpiord 5102  om2uz0i 6587  om2uzsuci 6588  seq1lem1 6602  seq1rval 6604  seq1suclem 6609  shftidt 6648  limsupval 6652  seq0valt 6659  seq1seq01 6667  seq00 6673  seq0p1 6674  cbvsumi 7109  sumeqfv 7120  fsumser0fi 7124  fsumser1fi 7125  serzfsum 7127  ser0cl 7169  ser1cl 7170  ser0mulci 7182  ser1mulci 7183  ser0cji 7188  iserzabslem 7301  isumval2 7317  isumcmpii 7338  geosumi 7364  efseq0ex 7434  effsumlei 7521  acdc3lem 7611  acdc2lem2 7614  acdc5lem2 7617  acdclem 7619  ruclem10 7644  ruclem11 7645  cnmetdval 8022  remetdval 8028  qdensere2 8036  fsumcnlem 8109  vafval 8341  bafval 8342  smfval 8343  0vfval 8344  nmfval 8345  vsfval 8373  shftefif1olem 8860  eflog 8879  logef 8881  logeftb 8883  avril1 8903  pjoc2i 9391  pjcji 9749  ho0val 9796  hoival 9801  hhbloi 9946  cnlnadjlem5 10121  adjbdlnb 10134  nmopcoadji 10151  hmopidmchlem 10195  hmopidmpji 10197  pjinvari 10237  pjadj2coi 10250  pj3lem1 10252  symgval 10524  oprabvaligg 10562  fvopab2a 10581  trnij 10773  domval 10790  codval 10791  idval 10792  cmpval 10793  rdmob 10816  homib 10859  ismona 10872

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-cnv 3241  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fv 3253

Copyright terms: Public domain