Theorem fveq2i 3733

Description: Equality inference for function value.

Hypothesis

Ref	Expression
fveq2i.1	|- A = B

Assertion

Ref	Expression
fveq2i	|- (F` A) = (F` B)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 |- A = B
2		fveq2 3730	. 2 |- (A = B -> (F` A) = (F` B))
3	1, 2	ax-mp 7	1 |- (F` A) = (F` B)

Syntax hints:   = wceq 958  ` cfv 3188

This theorem is referenced by:  tz7.44-1 3934  tz7.44-2 3935  inf3lemc 4620  rankid 4682  rankpr 4702  rankop 4703  ranksuc 4710  numthlem 4793  cardiun 4870  alephcard 4878  aleph1 4882  addclprlem2 5131  uzrdgini 6304  seq1lem1 6310  seq11lem 6316  seq1suclem 6317  seq00 6551  seq01 6553  sqr1 6717  sqrsq 6721  cjcj 6778  recj 6782  imcj 6783  readd 6784  imadd 6785  remul 6786  immul 6787  reneg 6794  imneg 6796  rei 6824  imi 6825  absval2 6841  abssub 6846  absmul 6847  absid 6861  absi 6878  abslem2i 6908  facp1t 6936  fac2 6937  fac3 6938  bcpasc2 6967  fsumshft 7031  ser0cj 7065  isumnn0nn 7207  cvgratlem2ALT 7248  ivthlem6 7286  ivthlem7 7287  isupivth 7290  efaddlem5 7342  efaddlem23 7360  efsep 7396  eflt 7406  efcnlem2 7420  sin0 7444  sin0ALT 7445  cos0 7446  sinadd 7451  cosadd 7452  cos2tOLD 7465  sin01bndlem1 7468  cos2bnd 7476  sin4lt0 7482  ruclem16 7526  ruclem25 7535  ruclem30 7540  ruclem31 7541  ruclem32 7542  aleph1re 7552  cnmetdval 7899  qdensere2 7913  oprcn 7974  fsumcnlem 7986  0vfval 8221  nvvop 8224  nvvc 8230  vsfval 8250  cnnvg 8304  cnnvs 8307  cnnvnm 8308  imsdval 8313  ipval2lem1 8347  ipval2 8353  ipid 8359  nmblolbii 8455  blocnilem 8460  ip0i 8480  ip1ilem 8481  ipasslem10 8495  siilem1 8507  cnbn 8524  pilem3 8668  sinhalfpilem 8674  cospi 8677  sincos4thpi 8705  sincos6thpi 8706  eflogt 8755  pilog 8763  h2hva 8838  h2hsm 8839  h2hnm 8840  axhfvadd 8847  axhvcom 8848  axhvass 8849  axhv0cl 8850  axhvaddid 8851  axhfvmul 8852  axhvmulid 8853  axhvmulass 8854  axhvdistr1 8855  axhvdistr2 8856  axhvmul0 8857  axhfi 8858  axhis1 8859  axhis2 8860  axhis3 8861  axhis4 8862  axhcompl 8863  norm-iii 9001  normsub 9003  norm3dif 9009  normpar2 9018  hh0v 9030  hhssva 9124  hhsssm 9125  hhssnm 9126  hhshsslem1 9132  hhsssh2 9135  occllem1 9168  projlem7 9187  projlem18 9198  pjthlem1 9214  pjthlem7 9220  pjthlem13 9226  pjoc2 9266  choc1 9286  dfchj3 9320  shjcomt 9325  shs0 9367  chj0 9373  chdmj1 9399  chjass 9404  chjo 9406  spansn0 9459  spanpr 9498  qlaxr4 9570  pjadj 9613  pjadd 9615  pjmul 9617  pjsub 9618  pjcj 9624  pjnorm 9661  pjpyth 9662  ho0valt 9671  lnop0t 9885  lnophmlem2 9937  nmbdoplb 9944  lnfn0 9966  nmopadj 10018  nmoptri2 10027  nmopcoadj2 10030  unierr 10032  branmfnt 10033  pjbdln 10071  pjclem2 10119  sto1 10158  stm1r 10166  st0 10171  hstrlem3a 10182  hstrlem4 10184  golem1 10193  superpos 10276  shatomistic 10283  ghomgrpilem2 10381  cayleylem3 10406  1ded 10642  homib 10695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204

Copyright terms: Public domain