Theorem breq2i 5078

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

Syntax hints:   ↔ wb 205   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breqtri  5095  en1  8765  en1OLD  8766  snnen2o  8903  enp1i  8982  pm54.43  9690  addclprlem2  10704  map2psrpr  10797  lt0neg2  11412  le0neg2  11414  recgt1  11801  addltmul  12139  nn0lt2  12313  3halfnz  12329  xlt0neg2  12883  xle0neg2  12885  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  hashen1  14013  swrdccatin2  14370  pfxccat3  14375  mertens  15526  aleph1re  15882  dvdslelem  15946  3dvdsdec  15969  3dvds2dec  15970  divalglem5  16034  ndvdsi  16049  bitsfzo  16070  absproddvds  16250  prmfac1  16354  prm23lt5  16443  dec2dvds  16692  dec5dvds2  16694  prmlem0  16735  dprd0  19549  ablfac1lem  19586  minveclem3b  24497  minveclem6  24503  minveclem7  24504  ioombl1lem4  24630  sinhalfpilem  25525  sincosq1lem  25559  sincosq1sgn  25560  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  bposlem6  26342  gausslemma2dlem1a  26418  2lgsoddprmlem3  26467  lfgrwlkprop  27957  konigsberglem4  28520  frgrwopreglem2  28578  avril1  28728  minvecolem5  29144  minvecolem6  29145  minvecolem7  29146  bcsiALT  29442  pjdifnormii  29946  cvexchi  30632  ballotlem4  32365  bnj110  32738  wsuclb  33749  nosupinfsep  33862  dalem18  37622  dalem48  37661  cdlemblem  37734  cdleme7ga  38189  cdlemg27b  38637  frege116  41476  frege120  41480  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  hoidmv1lelem3  44021  hoidmvlelem3  44025  hoidmvle  44028  257prm  44901  fmtno4prmfac  44912  fmtno4nprmfac193  44914  flsqrt5  44934  139prmALT  44936  31prm  44937  127prm  44939  lighneallem2  44946  stgoldbwt  45116  nnsum3primesle9  45134  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  lincdifsn  45653  lindslinindsimp1  45686  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  fldivexpfllog2  45799  nnlog2ge0lt1  45800  blen1b  45822  resum2sqorgt0  45943