Theorem breq2i 5110

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtri  5127  en1  8972  sdom1  9166  enp1i  9200  enp1iOLD  9201  pm54.43  9930  addclprlem2  10946  map2psrpr  11039  lt0neg2  11661  le0neg2  11663  recgt1  12055  inelr  12152  addltmul  12394  nn0lt2  12573  3halfnz  12589  xlt0neg2  13156  xle0neg2  13158  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  hashen1  14311  swrdccatin2  14670  pfxccat3  14675  mertens  15828  aleph1re  16189  dvdslelem  16255  3dvdsdec  16278  3dvds2dec  16279  divalglem5  16343  ndvdsi  16358  bitsfzo  16381  absproddvds  16563  prmfac1  16666  prm23lt5  16761  dec2dvds  17010  dec5dvds2  17012  prmlem0  17052  dprd0  19947  ablfac1lem  19984  minveclem3b  25361  minveclem6  25367  minveclem7  25368  ioombl1lem4  25495  sinhalfpilem  26405  sincosq1lem  26439  sincosq1sgn  26440  sincosq2sgn  26441  sincosq3sgn  26442  sincosq4sgn  26443  bposlem6  27233  gausslemma2dlem1a  27309  2lgsoddprmlem3  27358  nosupinfsep  27677  addscut  27925  slt0neg2d  27997  mulscut  28075  abssneg  28189  elnnzs  28329  avgslt1d  28379  avgslt2d  28380  lfgrwlkprop  29666  konigsberglem4  30234  frgrwopreglem2  30292  avril1  30442  minvecolem5  30860  minvecolem6  30861  minvecolem7  30862  bcsiALT  31158  pjdifnormii  31662  cvexchi  32348  fldext2chn  33711  ballotlem4  34483  bnj110  34841  wsuclb  35809  dalem18  39668  dalem48  39707  cdlemblem  39780  cdleme7ga  40235  cdlemg27b  40683  sn-inelr  42468  frege116  43961  frege120  43965  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  hoidmv1lelem3  46584  hoidmvlelem3  46588  hoidmvle  46591  257prm  47555  fmtno4prmfac  47566  fmtno4nprmfac193  47568  flsqrt5  47588  139prmALT  47590  31prm  47591  127prm  47593  lighneallem2  47600  stgoldbwt  47770  nnsum3primesle9  47788  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  lincdifsn  48406  lindslinindsimp1  48439  lindslinindsimp2lem5  48444  lindslinindsimp2  48445  fldivexpfllog2  48547  nnlog2ge0lt1  48548  blen1b  48570  resum2sqorgt0  48691