Theorem breq2i 2623

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

Syntax hints:   ↔ wb 146   = wceq 954   class class class wbr 2615

This theorem is referenced by:  breqtr 2634  en1 4424  pm54.43 4564  addclprlem2 5111  prlem934b 5130  mappsrpr 5210  ltmullem 5634  lt0neg2t 5662  le0neg2t 5664  prodge0 5796  recgt1t 5867  halfpos 5872  exple1t 6558  bcpasc 6927  ivthlem7 7242  isupivth 7245  ivthlem7OLD 7251  ivth2OLD 7254  eirrlem1 7350  efcnlem1 7379  efcnlem2 7380  ruclem3 7475  ruclem35 7507  aleph1re 7514  bcthlem17 7977  bcthlem33 7993  sinhalfpilem 8633  sincosq1lem 8655  sincosq1sgn 8656  sincosq2sgn 8657  sincosq3sgn 8658  sincosq4sgn 8659  efif1lem1 8680  efif1lem2 8681  efif1lem5 8684  avril1 8758  bcsALT 9020  projlem4 9163  pjdifnorm 9603  cvexch 10267

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 2616

Copyright terms: Public domain