Theorem breq2i 2622

Description: Equality inference for a 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 2618	. 2 |- (A = B -> (CRA <-> CRB))
3	1, 2	ax-mp 7	1 |- (CRA <-> CRB)

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

This theorem is referenced by:  breqtr 2633  en1 4413  pm54.43 4552  addclprlem2 5099  prlem934b 5118  mappsrpr 5198  ltmullem 5622  lt0neg2t 5650  le0neg2t 5652  prodge0 5784  recgt1t 5855  halfpos 5860  exple1t 6546  bcpasc 6915  ivthlem7 7230  isupivth 7233  ivthlem7OLD 7239  ivth2OLD 7242  eirrlem1 7338  efcnlem1 7367  efcnlem2 7368  ruclem3 7463  ruclem35 7495  aleph1re 7502  bcthlem17 7965  bcthlem33 7981  sinhalfpilem 8617  sincosq1lem 8639  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  efif1lem1 8664  efif1lem2 8665  efif1lem5 8668  avril1 8723  bcsALT 8985  projlem4 9128  pjdifnorm 9568  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