Theorem breq2i 2069

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 ⊢ AI/I> = B
2		breq2 2066	. 2 ⊢ (< >A = B → (CRA ↔ CRB))
3	1, 2	ax-mp 6	1 ⊢ (CRA ↔ CRB)

Syntax hints:   ↔ wb 127   = wceq 1091   class class class wbr 2054

This theorem is referenced by:  breq12i 2070  breqtr 2080  en1 3331  addclprlem2 3913  prlem934b 3932  mappsrpr 4012  ltsubadd2 4317  lesubadd 4319  posdif 4328  ltnegcon1 4332  ltmullem 4337  lt0neg2t 4371  le0neg2t 4373  divgt0lem 4389  ltdiv23i 4412  halfpos 4421  sqegt0 4703  ruclem3 4887  ruclem35 4919  bcs 5101  projlem4 5196  projlem6 5198  pjthlem3 5227  pjdifnorm 5574  cvexch 5760

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org