Theorem breq2i 5156

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

Syntax hints:   ↔ wb 206   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  breqtri  5173  en1  9063  snnen2oOLD  9262  sdom1  9276  enp1i  9311  enp1iOLD  9312  pm54.43  10039  addclprlem2  11055  map2psrpr  11148  lt0neg2  11768  le0neg2  11770  recgt1  12162  addltmul  12500  nn0lt2  12679  3halfnz  12695  xlt0neg2  13259  xle0neg2  13261  iccshftr  13523  iccshftl  13525  iccdil  13527  icccntr  13529  hashen1  14406  swrdccatin2  14764  pfxccat3  14769  mertens  15919  aleph1re  16278  dvdslelem  16343  3dvdsdec  16366  3dvds2dec  16367  divalglem5  16431  ndvdsi  16446  bitsfzo  16469  absproddvds  16651  prmfac1  16754  prm23lt5  16848  dec2dvds  17097  dec5dvds2  17099  prmlem0  17140  dprd0  20066  ablfac1lem  20103  minveclem3b  25476  minveclem6  25482  minveclem7  25483  ioombl1lem4  25610  sinhalfpilem  26520  sincosq1lem  26554  sincosq1sgn  26555  sincosq2sgn  26556  sincosq3sgn  26557  sincosq4sgn  26558  bposlem6  27348  gausslemma2dlem1a  27424  2lgsoddprmlem3  27473  nosupinfsep  27792  addscut  28026  slt0neg2d  28098  mulscut  28173  abssneg  28286  elnnzs  28402  lfgrwlkprop  29720  konigsberglem4  30284  frgrwopreglem2  30342  avril1  30492  minvecolem5  30910  minvecolem6  30911  minvecolem7  30912  bcsiALT  31208  pjdifnormii  31712  cvexchi  32398  fldext2chn  33734  ballotlem4  34480  bnj110  34851  wsuclb  35810  dalem18  39664  dalem48  39703  cdlemblem  39776  cdleme7ga  40231  cdlemg27b  40679  frege116  43969  frege120  43973  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  hoidmv1lelem3  46549  hoidmvlelem3  46553  hoidmvle  46556  257prm  47486  fmtno4prmfac  47497  fmtno4nprmfac193  47499  flsqrt5  47519  139prmALT  47521  31prm  47522  127prm  47524  lighneallem2  47531  stgoldbwt  47701  nnsum3primesle9  47719  wtgoldbnnsum4prm  47727  bgoldbnnsum3prm  47729  lincdifsn  48270  lindslinindsimp1  48303  lindslinindsimp2lem5  48308  lindslinindsimp2  48309  fldivexpfllog2  48415  nnlog2ge0lt1  48416  blen1b  48438  resum2sqorgt0  48559