Theorem breq1i 2621

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 2617	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	ax-mp 7	1 |- (ARC <-> BRC)

Syntax hints:   <-> wb 146   = wceq 954   class class class wbr 2614

This theorem is referenced by:  eqbrtr 2629  2dom 4414  0sdom1dom 4510  prfi 4537  pwfilem 4550  unxpdomlem 4823  gt0srpr 5167  mappsrpr 5198  ltpsrpr 5199  map2psrpr 5200  pre-axmulgt0 5270  ltsubadd 5576  addgt0 5580  ltnegcon2 5587  lesub0 5594  msqgt0 5595  ltmullem 5622  lt0neg1t 5649  le0neg1t 5651  lt2msq 5837  reclt1t 5854  halfpost 5991  elnn0nn 6126  recnzt 6146  dfuz 6158  uzindOLD 6164  uzwo3lem2 6173  seq1lem2 6255  bernneq 6591  nn0opthlem1 6602  faclbnd4lem1 6893  bcpasc 6915  cbvsum 6932  climuz0 7053  iserzshft 7088  ser1f0 7114  isumnn0nn 7150  isum0split 7160  geoisum1c 7188  cvgratlem2ALT 7191  isupivth 7233  ivthlem6OLD 7238  ivthlem7OLD 7239  ivth2OLD 7242  efseq1ex 7256  dfef2 7257  efseq0ex 7261  efclt 7262  efcvg 7264  efcvgfsum 7265  reefcl 7267  ef1tllem 7331  eirrlem1 7338  eirrlem4 7341  efcnlem1 7367  ruclem1 7461  ruclem8 7468  fctop 7600  bcthlem32 7980  sincosq1sgn 8640  sincosq3sgn 8642  sincosq4sgn 8643  hhblo 9768  cvexch 10233

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-12 966  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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615

Copyright terms: Public domain