Theorem breq1i 2616

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

Syntax hints:   <-> wb 146   = wceq 953   class class class wbr 2609

This theorem is referenced by:  eqbrtr 2624  2dom 4408  0sdom1dom 4504  prfi 4531  pwfilem 4544  unxpdomlem 4815  gt0srpr 5159  mappsrpr 5190  ltpsrpr 5191  map2psrpr 5192  pre-axmulgt0 5262  ltsubadd 5568  addgt0 5572  ltnegcon2 5579  lesub0 5586  msqgt0 5587  ltmullem 5614  lt0neg1t 5641  le0neg1t 5643  lt2msq 5829  reclt1t 5846  halfpost 5983  elnn0nn 6118  recnzt 6138  dfuz 6150  uzindOLD 6156  uzwo3lem2 6165  seq1lem2 6247  bernneq 6583  nn0opthlem1 6594  faclbnd4lem1 6885  bcpasc 6907  cbvsum 6924  climuz0 7045  iserzshft 7080  ser1f0 7106  isumnn0nn 7142  isum0split 7152  geoisum1c 7180  cvgratlem2ALT 7183  isupivth 7225  ivthlem6OLD 7230  ivthlem7OLD 7231  ivth2OLD 7234  efseq1ex 7248  dfef2 7249  efseq0ex 7253  efclt 7254  efcvg 7256  efcvgfsum 7257  reefcl 7259  ef1tllem 7323  eirrlem1 7330  eirrlem4 7333  efcnlem1 7359  ruclem1 7453  ruclem8 7460  fctop 7592  bcthlem32 7964  sincosq1sgn 8621  sincosq3sgn 8623  sincosq4sgn 8624  hhblo 9745  cvexch 10204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain