Theorem breq2i 3346

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 3342	. 2 |- (A = B -> (CRA <-> CRB))
3	1, 2	ax-mp 7	1 |- (CRA <-> CRB)

Syntax hints:   <-> wb 163   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  breqtri 3360  en1 5485  pm54.43 5662  elomsubsd 5885  addclprlem2 6271  prlem934b 6290  mappsrpr 6370  lesub0i 6792  ltmullem 6824  lt0neg2 6858  le0neg2 6860  prodge0i 6998  recgt1 7082  halfposi 7087  addltmul 7229  exple1 7852  bcpasci 8221  ivthlem7 8549  isupivthi 8552  eirrlem1 8651  efcnlem1 8684  efcnlem2 8685  ruclem3 8781  ruclem35 8813  aleph1re 8820  bcthlem17 9293  bcthlem33 9309  sinhalfpilem 10028  sincosq1lem 10052  sincosq1sgn 10053  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  efif1lem1 10084  efif1lem2 10085  efif1lem5 10088  avril1 10142  bcsiALT 10679  projlem4 10822  pjdifnormii 11263  cvexchi 11941  bnj33 12401  nn0lt10b 13603  dvdslelem 13692  divalglem5 13700  3prm 13780  top2usne 14898  elomsubsdOLD 15394  reconnlem3 15448  fsumleisumi 15826  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  pcoass 16085

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain