Theorem fveq2i 3666

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

Syntax hints:   = wceq 1099  ` cfv 3145

This theorem is referenced by:  tz7.44-1 3867  tz7.44-2 3868  inf3lemc 4535  rankid 4596  rankpr 4616  rankop 4617  ranksuc 4624  numthlem 4707  cardiun 4782  alephcard 4790  aleph1 4794  addclprlem2 5042  uzrdgini 6191  seq1lem1 6197  seq11lem 6203  seq1suclem 6204  seq00 6433  seq01 6435  sqr1 6597  sqrsq 6601  cjcj 6664  recj 6668  imcj 6669  readd 6670  imadd 6671  remul 6672  immul 6673  reneg 6680  imneg 6682  rei 6710  imi 6711  absval2 6727  abssub 6732  absmul 6733  absid 6747  absi 6766  abslem2i 6796  facp1t 6824  fac2 6825  fac3 6826  bcpasc2 6856  fsumshft 6920  ser0cj 6954  isumnn0nn 7093  cvgratlem2ALT 7134  ivthlem6 7172  ivthlem7 7173  isupivth 7176  ivthlem6OLD 7181  ivthlem7OLD 7182  efaddlem5 7235  efaddlem23 7253  efsep 7288  eflt 7298  efcnlem2 7311  sin0 7337  sin0ALT 7338  cos0 7339  sinadd 7344  cosadd 7345  cos2tOLD 7357  sin01bndlem1 7360  cos2bnd 7368  sin4lt0 7374  ruclem16 7419  ruclem25 7428  ruclem30 7433  ruclem31 7434  ruclem32 7435  aleph1re 7445  cnmetdval 7789  qdensere2 7803  oprcn 7859  fsumcnlem 7871  0vfval 8105  nvvop 8108  nvvc 8112  vsfval 8132  cnnvg 8183  cnnvs 8186  cnnvnm 8187  imsdval 8192  ipval2lem1 8220  ipval2 8226  ipid 8232  nmblolbii 8325  blocnilem 8330  ip0i 8350  ip1ilem 8351  ipasslem10 8365  siilem1 8377  cnbn 8394  pilem3 8505  sinhalfpilem 8511  cospi 8514  sincos4thpi 8540  sincos6thpi 8541  eflogt 8595  pilog 8603  eflogtOLD 8617  ghomgrpilem2 8653  cayleylem3 8678  1ded 8865  homib 8918  norm-iii 9155  normsub 9157  norm3dif 9163  normpar2 9172  hhva 9182  hh0v 9184  hhsm 9185  hhnm 9187  hhlm 9218  hhcau 9219  hhssva 9280  hhsssm 9281  hhssnm 9282  occllem1 9303  projlem7 9322  projlem18 9333  pjthlem1 9348  pjthlem7 9354  pjthlem13 9360  pjoc2 9400  choc1 9420  dfchj3 9454  shjcomt 9459  shs0 9501  chj0 9507  chdmj1 9533  chjass 9538  chjo 9540  spansn0 9593  spanpr 9634  qlaxr4 9706  pjadj 9749  pjadd 9751  pjmul 9753  pjsub 9754  pjcj 9760  pjnorm 9797  pjpyth 9798  ho0valt 9807  lnop0t 10020  lnophmlem2 10071  nmbdoplb 10078  lnfn0 10100  nmopadj 10152  nmoptri2 10160  nmopcoadj2 10163  unierr 10164  branmfnt 10165  pjbdln 10201  pjclem2 10248  sto1 10287  stm1r 10295  st0 10300  hstrlem3a 10311  hstrlem4 10313  golem1 10322  superpos 10403  shatomistic 10410

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161

Copyright terms: Public domain