Theorem fveq2i 3727

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

Syntax hints:   = wceq 956  ` cfv 3182

This theorem is referenced by:  tz7.44-1 3928  tz7.44-2 3929  inf3lemc 4611  rankid 4672  rankpr 4692  rankop 4693  ranksuc 4700  numthlem 4783  cardiun 4859  alephcard 4867  aleph1 4871  addclprlem2 5119  uzrdgini 6303  seq1lem1 6309  seq11lem 6315  seq1suclem 6316  seq00 6550  seq01 6552  sqr1 6716  sqrsq 6720  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 7464  sin01bndlem1 7467  cos2bnd 7475  sin4lt0 7481  ruclem16 7525  ruclem25 7534  ruclem30 7539  ruclem31 7540  ruclem32 7541  aleph1re 7551  cnmetdval 7902  qdensere2 7916  oprcn 7977  fsumcnlem 7989  0vfval 8225  nvvop 8228  nvvc 8234  vsfval 8254  cnnvg 8308  cnnvs 8311  cnnvnm 8312  imsdval 8317  ipval2lem1 8351  ipval2 8357  ipid 8363  nmblolbii 8459  blocnilem 8464  ip0i 8484  ip1ilem 8485  ipasslem10 8499  siilem1 8511  cnbn 8528  pilem3 8673  sinhalfpilem 8679  cospi 8682  sincos4thpi 8710  sincos6thpi 8711  eflogt 8760  pilog 8768  h2hva 8843  h2hsm 8844  h2hnm 8845  axhfvadd 8852  axhvcom 8853  axhvass 8854  axhv0cl 8855  axhvaddid 8856  axhfvmul 8857  axhvmulid 8858  axhvmulass 8859  axhvdistr1 8860  axhvdistr2 8861  axhvmul0 8862  axhfi 8863  axhis1 8864  axhis2 8865  axhis3 8866  axhis4 8867  axhcompl 8868  norm-iii 9006  normsub 9008  norm3dif 9014  normpar2 9023  hh0v 9035  hhssva 9129  hhsssm 9130  hhssnm 9131  hhshsslem1 9137  hhsssh2 9140  occllem1 9173  projlem7 9192  projlem18 9203  pjthlem1 9219  pjthlem7 9225  pjthlem13 9231  pjoc2 9271  choc1 9291  dfchj3 9325  shjcomt 9330  shs0 9372  chj0 9378  chdmj1 9404  chjass 9409  chjo 9411  spansn0 9464  spanpr 9503  qlaxr4 9575  pjadj 9618  pjadd 9620  pjmul 9622  pjsub 9623  pjcj 9629  pjnorm 9666  pjpyth 9667  ho0valt 9676  lnop0t 9890  lnophmlem2 9942  nmbdoplb 9949  lnfn0 9971  nmopadj 10023  nmoptri2 10032  nmopcoadj2 10035  unierr 10037  branmfnt 10038  pjbdln 10076  pjclem2 10124  sto1 10163  stm1r 10171  st0 10176  hstrlem3a 10187  hstrlem4 10189  golem1 10198  superpos 10281  shatomistic 10288  ghomgrpilem2 10386  cayleylem3 10411  1ded 10671  homib 10724

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-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198

Copyright terms: Public domain