Theorem breq2i 5121

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

Syntax hints:   ↔ wb 209   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  breqtri  5140  en1  9020  sdom1  9209  enp1i  9238  pm54.43  9986  addclprlem2  11001  map2psrpr  11094  lt0neg2  11720  le0neg2  11722  recgt1  12110  inelr  12207  addltmul  12479  nn0lt2  12658  3halfnz  12674  xlt0neg2  13245  xle0neg2  13247  iccshftr  13512  iccshftl  13514  iccdil  13516  icccntr  13518  hashen1  14405  swrdccatin2  14765  pfxccat3  14770  mertens  15939  aleph1re  16300  dvdslelem  16366  3dvdsdec  16389  3dvds2dec  16390  divalglem5  16454  ndvdsi  16469  bitsfzo  16492  absproddvds  16674  prmfac1  16778  prm23lt5  16873  dec2dvds  17122  dec5dvds2  17124  prmlem0  17164  dprd0  20102  ablfac1lem  20139  minveclem3b  25555  minveclem6  25561  minveclem7  25562  ioombl1lem4  25688  sinhalfpilem  26593  sincosq1lem  26627  sincosq1sgn  26628  sincosq2sgn  26629  sincosq3sgn  26630  sincosq4sgn  26631  bposlem6  27418  gausslemma2dlem1a  27494  2lgsoddprmlem3  27543  nosupinfsep  27861  addcuts  28136  lt0negs2d  28209  mulcut  28290  absnegs  28405  n0lts1e0  28526  elnnzs  28559  avglts1d  28611  avglts2d  28612  bdaypw2n0bndlem  28621  z12bdaylem1  28628  lfgrwlkprop  29975  konigsberglem4  30546  frgrwopreglem2  30604  avril1  30754  minvecolem5  31173  minvecolem6  31174  minvecolem7  31175  bcsiALT  31471  pjdifnormii  31975  cvexchi  32661  fldext2chn  34062  ballotlem4  34833  bnj110  35190  wsuclb  36216  dalem18  40344  dalem48  40383  cdlemblem  40456  cdleme7ga  40911  cdlemg27b  41359  sn-inelr  43150  frege116  44596  frege120  44600  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  hoidmv1lelem3  47198  hoidmvlelem3  47202  hoidmvle  47205  257prm  48201  fmtno4prmfac  48212  fmtno4nprmfac193  48214  flsqrt5  48234  139prmALT  48236  31prm  48237  127prm  48239  lighneallem2  48246  nprmdvdsfacm1lem2  48261  stgoldbwt  48429  nnsum3primesle9  48447  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  lincdifsn  49088  lindslinindsimp1  49121  lindslinindsimp2lem5  49126  lindslinindsimp2  49127  fldivexpfllog2  49229  nnlog2ge0lt1  49230  blen1b  49252  resum2sqorgt0  49373