Theorem fveq2i 2835

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

Syntax hints:   = wceq 1091  ` cfv 2422

This theorem is referenced by:  tz7.44-1 2966  tz7.44-2 2967  inf3lemc 3462  rankid 3516  rankpr 3536  numthlem 3598  cardiun 3665  alephcard 3673  aleph1 3676  addclprlem2 3913  uzrdgini 4658  seqlem1 4662  seq1lem 4668  seqsuclem 4669  sqr1 4771  sqrsqe 4774  cjcj 4808  recj 4812  imcj 4813  readd 4814  imadd 4815  remul 4816  immul 4817  reneg 4824  imneg 4826  absval2 4836  absneg 4843  abscj 4844  abssub 4845  absmul 4846  absid 4850  absre 4854  abs3dif 4860  abslem2i 4866  facp1t 4873  ruclem16 4900  ruclem25 4909  ruclem30 4914  ruclem31 4915  ruclem32 4916  norm-iii 5087  normsub 5089  norm3dif 5094  normpar2 5100  occllem1 5180  projlem7 5199  projlem18 5210  pjthlem1 5225  pjthlem7 5231  pjthlem13 5237  pjoc2 5273  choc1 5292  dfchj3 5326  shjcomt 5331  chj0 5377  chdmj1 5402  chjass 5407  chjo 5409  qlaxr4 5527  pjch0t 5562  pjadj 5564  pjadd 5566  pjmul 5568  pjsub 5569  pjcj 5575  pjoi0 5592  pjclem2 5650  pjnorm 5663  pjpyth 5664  sto1 5677  stm1r 5685  st0 5690  golem1 5704

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438

metamath.org