Theorem fveq2i 3729

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 3726	. 2 ⊢ (A = B → (F ‘A) = (F ‘B))
3	1, 2	ax-mp 7	1 ⊢ (F ‘A) = (F ‘B)

Syntax hints:   = wceq 954   ‘cfv 3182

This theorem is referenced by:  tz7.44-1 3930  tz7.44-2 3931  inf3lemc 4603  rankid 4664  rankpr 4684  rankop 4685  ranksuc 4692  numthlem 4775  cardiun 4851  alephcard 4859  aleph1 4863  addclprlem2 5111  uzrdgini 6260  seq1lem1 6266  seq11lem 6272  seq1suclem 6273  seq00 6502  seq01 6504  sqr1 6666  sqrsq 6670  cjcj 6733  recj 6737  imcj 6738  readd 6739  imadd 6740  remul 6741  immul 6742  reneg 6749  imneg 6751  rei 6779  imi 6780  absval2 6796  abssub 6801  absmul 6802  absid 6816  absi 6835  abslem2i 6865  facp1t 6893  fac2 6894  fac3 6895  bcpasc2 6925  fsumshft 6989  ser0cj 7023  isumnn0nn 7162  cvgratlem2ALT 7203  ivthlem6 7241  ivthlem7 7242  isupivth 7245  ivthlem6OLD 7250  ivthlem7OLD 7251  efaddlem5 7304  efaddlem23 7322  efsep 7357  eflt 7367  efcnlem2 7380  sin0 7406  sin0ALT 7407  cos0 7408  sinadd 7413  cosadd 7414  cos2tOLD 7426  sin01bndlem1 7429  cos2bnd 7437  sin4lt0 7443  ruclem16 7488  ruclem25 7497  ruclem30 7502  ruclem31 7503  ruclem32 7504  aleph1re 7514  cnmetdval 7866  qdensere2 7880  oprcn 7939  fsumcnlem 7951  0vfval 8191  nvvop 8194  nvvc 8202  vsfval 8222  cnnvg 8275  cnnvs 8278  cnnvnm 8279  imsdval 8284  ipval2lem1 8314  ipval2 8320  ipid 8326  nmblolbii 8419  blocnilem 8424  ip0i 8444  ip1ilem 8445  ipasslem10 8459  siilem1 8471  cnbn 8488  pilem3 8627  sinhalfpilem 8633  cospi 8636  sincos4thpi 8662  sincos6thpi 8663  eflogt 8717  pilog 8725  eflogtOLD 8739  h2hva 8817  h2hsm 8818  h2hnm 8819  axhfvadd 8826  axhvcom 8827  axhvass 8828  axhv0cl 8829  axhvaddid 8830  axhfvmul 8831  axhvmulid 8832  axhvmulass 8833  axhvdistr1 8834  axhvdistr2 8835  axhvmul0 8836  axhfi 8837  axhis1 8838  axhis2 8839  axhis3 8840  axhis4 8841  axhcompl 8842  norm-iii 8980  normsub 8982  norm3dif 8988  normpar2 8997  hh0v 9009  hhssva 9103  hhsssm 9104  hhssnm 9105  hhshsslem1 9111  hhsssh2 9114  occllem1 9147  projlem7 9166  projlem18 9177  pjthlem1 9192  pjthlem7 9198  pjthlem13 9204  pjoc2 9244  choc1 9264  dfchj3 9298  shjcomt 9303  shs0 9345  chj0 9351  chdmj1 9377  chjass 9382  chjo 9384  spansn0 9437  spanpr 9478  qlaxr4 9550  pjadj 9593  pjadd 9595  pjmul 9597  pjsub 9598  pjcj 9604  pjnorm 9641  pjpyth 9642  ho0valt 9651  lnop0t 9864  lnophmlem2 9915  nmbdoplb 9922  lnfn0 9944  nmopadj 9996  nmoptri2 10005  nmopcoadj2 10008  unierr 10010  branmfnt 10011  pjbdln 10049  pjclem2 10097  sto1 10136  stm1r 10144  st0 10149  hstrlem3a 10160  hstrlem4 10162  golem1 10171  superpos 10252  shatomistic 10259  ghomgrpilem2 10354  cayleylem3 10381  1ded 10587  homib 10640

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2699  ax-pow 2738  ax-pr 2775

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2500  df-br 2616  df-opab 2663  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