Theorem fveq2i 3803

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

Syntax hints:   = wceq 988  ` cfv 3237

This theorem is referenced by:  tz7.44-1 4004  tz7.44-2 4005  inf3lemc 4697  rankid 4758  rankpr 4778  rankop 4779  ranksuc 4786  numthlem 4869  cardiun 4948  alephcard 4956  aleph1 4960  addclprlem2 5208  uzrdginii 6596  seq1lem1 6602  seq11lem 6608  seq1suclem 6609  seq00 6673  seq01 6675  sqr1 6839  sqrsqi 6843  cjcji 6901  recji 6905  imcji 6906  readdi 6907  imaddi 6908  remuli 6909  immuli 6910  renegi 6917  imnegi 6919  rei 6947  imi 6948  absval2i 6964  abssubi 6969  absmuli 6970  absidi 6984  absi 7001  abslem2i 7031  facp1 7059  fac2 7060  fac3 7061  bcpasc2i 7090  fsumshft 7154  ser0cji 7188  isumnn0nn 7330  cvgratlem2ALT 7371  ivthlem6 7409  ivthlem7 7410  isupivthi 7413  efaddlem5 7465  efaddlem23 7483  efsepi 7520  eflti 7530  efcnlem2 7544  sin0 7568  sin0ALT 7569  cos0 7570  sinaddi 7575  cosaddi 7576  cos2OLD 7589  sin01bndlem1 7592  cos2bnd 7600  sin4lt0 7606  ruclem16 7650  ruclem25 7659  ruclem30 7664  ruclem31 7665  ruclem32 7666  aleph1re 7676  cnmetdval 8022  qdensere2 8036  oprcn 8097  fsumcnlem 8109  0vfval 8344  nvvop 8347  nvvc 8353  vsfval 8373  cnnvg 8427  cnnvs 8430  cnnvnm 8431  imsdval 8436  ipval2lem1 8470  ipval2 8476  ipid 8482  nmblolbii 8578  blocnilem 8583  ip0i 8603  ip1ilem 8604  ipasslem10 8618  siilem1 8630  cnbn 8647  pilem3 8791  sinhalfpilem 8797  cospi 8800  sincos4thpi 8829  sincos6thpi 8830  eflog 8879  pilog 8887  h2hva 8962  h2hsm 8963  h2hnm 8964  axhfvadd 8971  axhvcom 8972  axhvass 8973  axhv0cl 8974  axhvaddid 8975  axhfvmul 8976  axhvmulid 8977  axhvmulass 8978  axhvdistr1 8979  axhvdistr2 8980  axhvmul0 8981  axhfi 8982  axhis1 8983  axhis2 8984  axhis3 8985  axhis4 8986  axhcompl 8987  norm-iii.i 9126  normsubi 9128  norm3difi 9134  normpar2i 9143  hh0v 9155  hhssva 9249  hhsssm 9250  hhssnm 9251  hhshsslem1 9257  hhsssh2 9260  occllem1 9293  projlem7 9312  projlem18 9323  pjthlem1 9339  pjthlem7 9345  pjthlem13 9351  pjoc2i 9391  choc1 9411  dfchj3 9445  shjcom 9450  shs0i 9492  chj0i 9498  chdmj1i 9524  chjassi 9529  chjoi 9531  spansn0 9584  spanpr 9623  qlaxr4i 9695  pjadjii 9738  pjaddii 9740  pjmulii 9742  pjsubii 9743  pjcji 9749  pjnormi 9786  pjpythi 9787  ho0val 9796  lnop0 10007  lnophmlem2 10059  nmbdoplbi 10066  lnfn0i 10088  nmopadji 10140  nmoptri2i 10149  nmopcoadj2i 10152  unierri 10154  branmfn 10155  pjbdlni 10193  pjclem2 10242  sto1i 10281  stm1ri 10289  st0 10294  hstrlem3a 10305  hstrlem4 10307  golem1 10316  superpos 10399  shatomistici 10406  ghomgrpilem2 10507  cayleylem3 10532  1ded 10806  homib 10859

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-xp 3239  df-cnv 3241  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fv 3253

Copyright terms: Public domain