Theorem fveq2i 3838

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

Syntax hints:   = wceq 992  ` cfv 3263

This theorem is referenced by:  tz7.44-1 4229  tz7.44-2 4230  inf3lemc 4756  rankid 4818  rankpr 4838  rankop 4839  ranksuc 4846  numthlem 4929  cardiun 5009  alephcard 5017  aleph1 5021  addclprlem2 5273  uzrdginii 6667  cardfz 6671  seq1lem1 6674  seq11lem 6680  seq1suclem 6681  seq00 6745  seq01 6747  sqr1 6917  sqrsqi 6921  cjcji 6979  recji 6983  imcji 6984  readdi 6985  imaddi 6986  remuli 6987  immuli 6988  renegi 6995  imnegi 6997  rei 7025  imi 7026  absval2i 7043  abssubi 7048  absmuli 7049  absidi 7063  absi 7081  abslem2i 7111  facp1 7139  fac2 7140  fac3 7141  bcpasc2i 7170  fsumshft 7234  ser0cji 7268  isumnn0nn 7411  cvgratlem2ALT 7453  ivthlem6 7491  ivthlem7 7492  isupivthi 7495  efaddlem5 7547  efaddlem23 7565  efsepi 7604  eflti 7614  efcnlem2 7628  sin0 7652  sin0ALT 7653  cos0 7654  sinaddi 7659  cosaddi 7660  cos2OLD 7673  sin01bndlem1 7676  cos2bnd 7684  sin4lt0 7690  ruclem16 7737  ruclem25 7746  ruclem30 7751  ruclem31 7752  ruclem32 7753  aleph1re 7763  cnmetdval 8113  qdensere2 8127  oprcn 8188  fsumcnlem 8200  0vfval 8472  nvvop 8475  nvvc 8481  vsfval 8501  cnnvg 8555  cnnvs 8558  cnnvnm 8559  imsdval 8564  ipval2lem1 8605  ipval2 8611  ipid 8617  nmblolbii 8714  blocnilem 8719  ip0i 8740  ip1ilem 8741  ipasslem10 8755  siilem1 8767  cnbn 8786  pilem3 8940  sinhalfpilem 8946  cospi 8949  sincos4thpi 8978  sincos6thpi 8979  sinkpi 8981  eflog 9032  pilog 9040  h2hva 9118  h2hsm 9119  h2hnm 9120  axhfvadd 9127  axhvcom 9128  axhvass 9129  axhv0cl 9130  axhvaddid 9131  axhfvmul 9132  axhvmulid 9133  axhvmulass 9134  axhvdistr1 9135  axhvdistr2 9136  axhvmul0 9137  axhfi 9138  axhis1 9139  axhis2 9140  axhis3 9141  axhis4 9142  axhcompl 9143  norm-iii.i 9282  normsubi 9284  norm3difi 9290  normpar2i 9299  hh0v 9311  hhssva 9405  hhsssm 9406  hhssnm 9407  hhshsslem1 9413  hhsssh2 9416  occllem1 9449  projlem7 9468  projlem18 9479  pjthlem1 9495  pjthlem7 9501  pjthlem13 9507  pjoc2i 9547  choc1 9567  dfchj3 9601  shjcom 9606  shs0i 9648  chj0i 9654  chdmj1i 9680  chjassi 9685  chjoi 9687  spansn0 9740  spanpr 9779  qlaxr4i 9853  pjadjii 9896  pjaddii 9898  pjmulii 9900  pjsubii 9901  pjcji 9907  pjnormi 9944  pjpythi 9945  ho0val 9956  lnop0 10169  lnophmlem2 10221  nmbdoplbi 10228  lnfn0i 10250  nmopadji 10302  nmoptri2i 10311  nmopcoadj2i 10314  unierri 10316  branmfn 10317  branmfnOLD 10318  pjbdlni 10356  pjclem2 10405  sto1i 10444  stm1ri 10452  st0 10457  hstrlem3a 10468  hstrlem4 10470  golem1 10479  superpos 10562  shatomistici 10569  ghomgrpilem2 10671  cayleylem3 10696  expm 10937  ring1cl 10966  1ded 11192  homib 11251  omsubsuc 11438  clsun 11465  subcls 11481  subntr 11482  ivthALT 11515  fsumltisumi 11886  piececn 11955  heiborlem30 12040  heiborlem33 12043  heiborlem35 12045  bfplem6 12059  ismrer1 12080  icccmp 12083  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279

Copyright terms: Public domain