Theorem fveq1d 3726

Description: Equality deduction for function value.

Hypothesis

Ref	Expression
fveq1d.1	|- (ph -> F = G)

Assertion

Ref	Expression
fveq1d	|- (ph -> (F` A) = (G` A))

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 |- (ph -> F = G)
2		fveq1 3723	. 2 |- (F = G -> (F` A) = (G` A))
3	1, 2	syl 10	1 |- (ph -> (F` A) = (G` A))

Syntax hints:   -> wi 3   = wceq 956  ` cfv 3182

This theorem is referenced by:  hbfvd 3730  hbfvd2 3731  funssfv 3735  csbfv12g 3742  csbfv2g 3743  f1ocnvfv1 3878  f1ocnvfv2 3879  rdgeq1 3934  rdgeq2 3935  rdg0t 3944  curry1val 4100  oav 4150  mapenlem1 4489  mapxpen 4495  xpmapenlem2 4497  xpmapenlem4 4499  xpmapenlem5 4500  unidom 4808  seq1val 6312  shftvalt 6346  shftcan1t 6354  seqzvalt 6540  seqz1 6547  seqzp1 6548  seqzval2t 6553  expvalt 6570  sumeq2 6985  dffsum 6998  fsumserz 6999  climconst3 7096  clim2serz 7145  ef1tlub 7382  ef01tlub 7386  absef01tlub 7388  ef4pt 7400  ntrval 7676  clsval 7677  neival 7717  lpfval 7742  lpval 7743  cnpval 7759  bcth 8032  grpinvval 8067  grpdivfval 8081  grplactval 8097  imsdval 8317  ipfval 8352  sspnval 8396  nmofval 8425  nmoval 8426  bloval 8441  0oval 8448  nmlno0 8455  hmoval 8470  ubthlem1 8529  ubthi 8544  htthlem4 8623  pjvalt 9239  axpjpjt 9256  pjoc1t 9267  pjoc2t 9272  hosvalt 9516  hosvaltOLD 9517  homvalt 9518  hodvalt 9519  hodvaltOLD 9520  hfsvalt 9521  hfmvalt 9522  pjige0t 9636  pjcjt2 9637  pjcht 9639  pjsumt 9655  pjds 9657  pjds3 9658  pjopytht 9665  pjnormt 9669  pjpytht 9670  pjnelt 9671  bravalvalt 9868  kbvalvalt 9878  eigvalt 9884  leopg 10055  leoppost 10059  leoprf2t 10060  leoprft 10061  pj3cor1 10137  strlem2 10178  hstrlem2 10186  sfvlim 10605  sfvlimOLD 10606  limfillem2OLD 10608  cnvtr 10638  ishoma 10715  ishomd 10718  ismona 10737  isepia 10747  isfuna 10754

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