Theorem breq2i 5038

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 5034	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)

Syntax hints:   ↔ wb 209   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  breqtri  5055  en1  8559  snnen2o  8691  enp1i  8737  pm54.43  9414  addclprlem2  10428  map2psrpr  10521  lt0neg2  11136  le0neg2  11138  recgt1  11525  addltmul  11861  nn0lt2  12033  3halfnz  12049  xlt0neg2  12601  xle0neg2  12603  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  hashen1  13727  swrdccatin2  14082  pfxccat3  14087  mertens  15234  aleph1re  15590  dvdslelem  15651  3dvdsdec  15673  3dvds2dec  15674  divalglem5  15738  ndvdsi  15753  bitsfzo  15774  absproddvds  15951  prmfac1  16053  prm23lt5  16141  dec2dvds  16389  dec5dvds2  16391  prmlem0  16431  dprd0  19146  ablfac1lem  19183  minveclem3b  24032  minveclem6  24038  minveclem7  24039  ioombl1lem4  24165  sinhalfpilem  25056  sincosq1lem  25090  sincosq1sgn  25091  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  bposlem6  25873  gausslemma2dlem1a  25949  2lgsoddprmlem3  25998  lfgrwlkprop  27477  konigsberglem4  28040  frgrwopreglem2  28098  avril1  28248  minvecolem5  28664  minvecolem6  28665  minvecolem7  28666  bcsiALT  28962  pjdifnormii  29466  cvexchi  30152  ballotlem4  31866  bnj110  32240  wsuclb  33228  dalem18  36977  dalem48  37016  cdlemblem  37089  cdleme7ga  37544  cdlemg27b  37992  frege116  40680  frege120  40684  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  hoidmv1lelem3  43232  hoidmvlelem3  43236  hoidmvle  43239  257prm  44078  fmtno4prmfac  44089  fmtno4nprmfac193  44091  flsqrt5  44111  139prmALT  44113  31prm  44114  127prm  44116  lighneallem2  44124  stgoldbwt  44294  nnsum3primesle9  44312  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  lincdifsn  44833  lindslinindsimp1  44866  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  fldivexpfllog2  44979  nnlog2ge0lt1  44980  blen1b  45002  resum2sqorgt0  45123