Theorem breq2i 5082

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  breqtri  5099  en1  8811  en1OLD  8812  snnen2oOLD  9010  enp1i  9052  pm54.43  9759  addclprlem2  10773  map2psrpr  10866  lt0neg2  11482  le0neg2  11484  recgt1  11871  addltmul  12209  nn0lt2  12383  3halfnz  12399  xlt0neg2  12954  xle0neg2  12956  iccshftr  13218  iccshftl  13220  iccdil  13222  icccntr  13224  hashen1  14085  swrdccatin2  14442  pfxccat3  14447  mertens  15598  aleph1re  15954  dvdslelem  16018  3dvdsdec  16041  3dvds2dec  16042  divalglem5  16106  ndvdsi  16121  bitsfzo  16142  absproddvds  16322  prmfac1  16426  prm23lt5  16515  dec2dvds  16764  dec5dvds2  16766  prmlem0  16807  dprd0  19634  ablfac1lem  19671  minveclem3b  24592  minveclem6  24598  minveclem7  24599  ioombl1lem4  24725  sinhalfpilem  25620  sincosq1lem  25654  sincosq1sgn  25655  sincosq2sgn  25656  sincosq3sgn  25657  sincosq4sgn  25658  bposlem6  26437  gausslemma2dlem1a  26513  2lgsoddprmlem3  26562  lfgrwlkprop  28055  konigsberglem4  28619  frgrwopreglem2  28677  avril1  28827  minvecolem5  29243  minvecolem6  29244  minvecolem7  29245  bcsiALT  29541  pjdifnormii  30045  cvexchi  30731  ballotlem4  32465  bnj110  32838  wsuclb  33822  nosupinfsep  33935  dalem18  37695  dalem48  37734  cdlemblem  37807  cdleme7ga  38262  cdlemg27b  38710  frege116  41587  frege120  41591  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  hoidmv1lelem3  44131  hoidmvlelem3  44135  hoidmvle  44138  257prm  45013  fmtno4prmfac  45024  fmtno4nprmfac193  45026  flsqrt5  45046  139prmALT  45048  31prm  45049  127prm  45051  lighneallem2  45058  stgoldbwt  45228  nnsum3primesle9  45246  wtgoldbnnsum4prm  45254  bgoldbnnsum3prm  45256  lincdifsn  45765  lindslinindsimp1  45798  lindslinindsimp2lem5  45803  lindslinindsimp2  45804  fldivexpfllog2  45911  nnlog2ge0lt1  45912  blen1b  45934  resum2sqorgt0  46055