Theorem breq2i 2595

Description: Equality inference for binary relation.

Hypothesis

Ref	Expression
breq1i.1	|- A = B

Assertion

Ref	Expression
breq2i	|- (CRA <-> CRB)

Proof of Theorem breq2i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq2 2591	. 2 |- (A = B -> (CRA <-> CRB))
3	1, 2	ax-mp 7	1 |- (CRA <-> CRB)

Syntax hints:   <-> wb 146   = wceq 1099   class class class wbr 2587

This theorem is referenced by:  breqtr 2606  en1 4361  pm54.43 4498  addclprlem2 5042  prlem934b 5061  mappsrpr 5141  ltmullem 5565  lt0neg2t 5593  le0neg2t 5595  prodge0 5727  recgt1t 5798  halfpos 5803  exple1t 6489  bcpasc 6858  ivthlem7 7173  isupivth 7176  ivthlem7OLD 7182  ivth2OLD 7185  eirrlem1 7281  efcnlem1 7310  efcnlem2 7311  ruclem3 7406  ruclem35 7438  aleph1re 7445  bcthlem17 7897  bcthlem33 7913  sinhalfpilem 8511  sincosq1lem 8533  sincosq1sgn 8534  sincosq2sgn 8535  sincosq3sgn 8536  sincosq4sgn 8537  efif1lem1 8558  efif1lem2 8559  efif1lem5 8562  avril1 8964  bcsALT 9195  projlem4 9319  pjdifnorm 9759  cvexch 10418

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-un 2021  df-sn 2383  df-pr 2384  df-op 2387  df-br 2588

Copyright terms: Public domain