Theorem fveq1i 4682

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

Syntax hints:   = wceq 1298  ` cfv 3998

This theorem is referenced by:  fvopab3ig 4741  fvopab4gf 4744  fvopabgf 4750  fvopabnf 4751  fvsnun1 4764  fvsnun2 4765  elrnopabg 4773  fopab2 4796  rnssopab 4798  fopabco 4805  abrexexlem2 4835  oprabval 4952  oprabvalig 4953  1stval 5022  2ndval 5023  curry1 5075  curry2 5078  dfrdg2 5141  rdgval 5148  rdgsucopab 5154  rdgsucopabn 5155  frsucopab 5162  abianfplem 5170  xpmapenlem5 5594  unblem2 5634  ordtypelem1 5684  ordtypelem6 5689  inf3lema 5715  inf3lemb 5716  inf3lemc 5717  trcl 5752  r10 5762  r1lim 5764  tz9.12lem3 5772  rankval 5779  oncardval 5865  aleph0 5874  alephlim 5875  omsubsuc 5877  ac6lem 5916  numthlem 5945  zorn2lem1 5950  cardval 5975  alephfplem1 6044  addpiord 6164  mulpiord 6165  om2uz0i 7706  om2uzsuci 7707  seq1lem1 7722  seq1rval 7724  seq1suclem 7729  shftidt 7768  limsupval 7772  seq0valt 7779  seq1seq01 7787  seq00 7793  seq0p1 7794  hashgval 8230  cbvsumi 8246  sumeqfv 8257  fsumser0fi 8261  fsumser1fi 8262  serzfsum 8264  ser0cl 8306  ser1cl 8307  ser0mulci 8319  ser1mulci 8320  ser0cji 8325  iserzabslem 8438  isumval2 8455  isumcmpii 8476  geosumi 8503  efseq0ex 8573  effsumlei 8662  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  ruclem10 8788  ruclem11 8789  cnmetdval 9180  remetdval 9186  qdensere2 9194  fsumcnlem 9267  gid0 9338  grpidval 9342  vafval 9554  bafval 9555  smfval 9556  0vfval 9557  nmfval 9558  vsfval 9586  vacnlem6 9672  shftefif1olem 10095  eflog 10114  logef 10116  logeftb 10118  avril1 10142  oprabvaligg 10154  symgval 10202  upxp 10225  fgf 10283  pjoc2i 10904  pjcji 11264  ho0val 11313  hoival 11318  hhbloi 11465  cnlnadjlem5 11641  adjbdlnb 11654  nmopcoadji 11671  opsqrlem2 11712  opsqrlem5 11715  hmopidmchlem 11722  hmopidmpji 11724  pjinvari 11764  pjadj2coi 11777  pj3lem1 11779  seq1resval 13617  seq1resval2 13618  seq0cl 13620  algrf 13739  algr0 13740  algrp1 13742  frsucopabn 13911  wfrlem5 13961  fvopab2b 14476  gepsup 14593  seinf 14594  cbvprodi 14662  prodeqfv 14669  expmiz 14724  expm 14725  fnopabco2b 14734  trooo 14758  trinv 14759  trnij 15015  domval 15070  codval 15071  idval 15072  cmpval 15073  rdmob 15095  homib 15145  ismona 15158  issubcat 15193  tarval2 15249  valtar 15260  fictblem 15370  fictb 15371  ordtypelem1OLD 15375  ordtypelem6OLD 15380  omsubsucOLD 15386  subcls 15424  subntr 15425  neibastop2lem4 15522  sfcls 15604  tailf 15633  fvopabf4g 15703  oprabvalg 15706  fsumleisumi 15826  piececn 15894  cnopropabco 15917  cnoprab1 15921  cnoprab2 15922  bfplem2 15999  bfplem3 16000  pcorev 16087

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014

Copyright terms: Public domain