Theorem breq2i 3997

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
breq2i	⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)

Proof of Theorem breq2i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq2 3993	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)

Syntax hints:   ↔ wb 104   = wceq 1348   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breqtri  4014  en1  6777  snnen2og  6837  1nen2  6839  pm54.43  7167  caucvgprprlemval  7650  caucvgprprlemmu  7657  caucvgsr  7764  pitonnlem1  7807  lt0neg2  8388  le0neg2  8390  negap0  8549  recexaplem2  8570  recgt1  8813  crap0  8874  addltmul  9114  nn0lt10b  9292  nn0lt2  9293  3halfnz  9309  xlt0neg2  9796  xle0neg2  9798  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fihashen1  10734  cjap0  10871  abs00ap  11026  xrmaxiflemval  11213  mertenslem2  11499  mertensabs  11500  3dvdsdec  11824  3dvds2dec  11825  ndvdsi  11892  3prm  12082  prmfac1  12106  prm23lt5  12217  sinhalfpilem  13506  sincosq1lem  13540  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  logrpap0b  13591