Theorem breq1i 2626

Description: Equality inference for a binary relation.

Hypothesis

Ref	Expression
breq1i.1	|- A = B

Assertion

Ref	Expression
breq1i	|- (ARC <-> BRC)

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq1 2622	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	ax-mp 7	1 |- (ARC <-> BRC)

Syntax hints:   <-> wb 146   = wceq 956   class class class wbr 2619

This theorem is referenced by:  eqbrtr 2634  2dom 4427  0sdom1dom 4525  prfiOLD 4556  pwfilemOLD 4570  unxpdomlem 4843  gt0srpr 5187  mappsrpr 5218  ltpsrpr 5219  map2psrpr 5220  pre-axmulgt0 5290  ltsubadd 5594  addgt0 5598  ltnegcon2 5605  lesub0 5612  msqgt0 5613  ltmullem 5640  lt0neg1t 5668  le0neg1t 5670  lt2msq 5881  reclt1t 5898  halfpost 6036  elnn0nn 6171  recnzt 6191  dfuz 6202  uzindOLD 6208  uzwo3lem2 6217  seq1lem2 6310  bernneq 6652  nn0opthlem1 6664  faclbnd4lem1 6948  bcpasc 6969  cbvsum 6986  climuz0 7108  iserzshft 7144  ser1f0 7170  isum1clim 7197  isumnn0nn 7207  isum0split 7217  geoisum1c 7245  cvgratlem2ALT 7248  isupivth 7290  efseq1ex 7306  dfef2 7307  efseq0ex 7311  efclt 7312  efcvg 7314  efcvgfsum 7315  reefcl 7317  ef1tllem 7381  eirrlem1 7389  eirrlem4 7392  efcnlem1 7419  ruclem1 7510  ruclem8 7517  fctopOLD 7650  bcthlem32 8030  sincosq1sgn 8704  sincosq3sgn 8706  sincosq4sgn 8707  hhblo 9828  cvexch 10296  unpde2eg2 10544

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain