Theorem opreq1i 3009

Description: Equality inference for operations.

Hypothesis

Ref	Expression
opreq1i.1	|- A = B

Assertion

Ref	Expression
opreq1i	|- (AFC) = (BFC)

Proof of Theorem opreq1i

Step	Hyp	Ref	Expression
1		opreq1i.1	. 2 |- A = B
2		opreq1 3006	. 2 |- (A = B -> (AFC) = (BFC))
3	1, 2	ax-mp 6	1 |- (AFC) = (BFC)

Syntax hints:   = wceq 1091  (class class class)co 3001

This theorem is referenced by:  opreq12i 3011  caopr12 3075  caopr411 3079  map1 3335  cdaassen 3725  distrpq 3861  ltapq 3870  ltmpq 3871  ltexpq 3874  halfpq 3876  addclprlem2 3913  prlem934a 3931  m1m1sr 3996  recexsrlem 4006  axrecex 4079  axi2m1 4082  axcnre 4087  negneg 4154  mul12 4178  mulneg1 4190  div23 4244  divcan4 4248  divcan4z 4250  recrec 4253  rec11i 4261  divmul13 4267  recdivt 4270  divdiv23 4272  ltadd2 4312  ltneg 4330  prodgt0i 4387  nnsub 4450  2p2e4 4488  2times 4489  3p2e5 4492  3p3e6 4493  4p2e6 4494  4p3e7 4495  4p4e8 4496  5p2e7 4497  5p3e8 4498  5p4e9 4499  6p2e8 4500  6p3e9 4501  7p2e9 4502  isqm1 4525  crulem 4528  crmult 4530  rimul 4534  uzind 4603  om2uzsuc 4652  sqreci 4690  cu2 4711  binom 4712  discrlem1 4713  nneo 4719  nnesq 4720  nn0opthlem1 4722  nn0opth2 4725  sqrlem11 4741  sqrlem16 4746  cjcj 4808  cjadd 4818  cjmul 4819  cjneg 4827  absvalsq 4837  releabs 4858  abslem2i 4866  ruclem1 4885  ruclem2 4886  ruclem3 4887  ruclem15 4899  hvsubidt 5005  hvmulcom 5021  hvmul2neg 5022  hvsubass 5027  hvadd12 5029  hv2times 5033  hvnegdi 5034  hvaddcan 5037  hizer1t 5054  normlem0 5062  normlem1 5063  normlem3 5065  normlem8 5071  bcseq 5073  normsq 5082  norm-ii 5086  normsub 5089  norm3dif 5094  norm3adif 5095  normpar2 5100  occllem1 5180  projlem3 5195  projlem4 5196  projlem18 5210  pjthlem1 5225  pjthlem5 5229  pjthlem6 5230  pjthlem7 5231  chdmm2 5399  spanunsn 5482  fh2 5519  qlaxr5 5528  spansnj 5539  pjadj 5564  pjinorm 5567  pjsslem 5570  hos12 5608  hosd 5622  hosd1 5623  hosd2 5624  pjclem3 5651  pjpyth 5664  stadd3 5689  cvexchlem 5759  mdsymlem1 5776

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  df-opr 3003

metamath.org