Theorem breq2i 5107

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  breqtri  5124  en1  8965  sdom1  9154  enp1i  9183  pm54.43  9917  addclprlem2  10932  map2psrpr  11025  lt0neg2  11648  le0neg2  11650  recgt1  12042  inelr  12139  addltmul  12381  nn0lt2  12559  3halfnz  12575  xlt0neg2  13139  xle0neg2  13141  iccshftr  13406  iccshftl  13408  iccdil  13410  icccntr  13412  hashen1  14297  swrdccatin2  14656  pfxccat3  14661  mertens  15813  aleph1re  16174  dvdslelem  16240  3dvdsdec  16263  3dvds2dec  16264  divalglem5  16328  ndvdsi  16343  bitsfzo  16366  absproddvds  16548  prmfac1  16651  prm23lt5  16746  dec2dvds  16995  dec5dvds2  16997  prmlem0  17037  dprd0  19966  ablfac1lem  20003  minveclem3b  25388  minveclem6  25394  minveclem7  25395  ioombl1lem4  25522  sinhalfpilem  26432  sincosq1lem  26466  sincosq1sgn  26467  sincosq2sgn  26468  sincosq3sgn  26469  sincosq4sgn  26470  bposlem6  27260  gausslemma2dlem1a  27336  2lgsoddprmlem3  27385  nosupinfsep  27704  addcuts  27978  lt0negs2d  28051  mulcut  28132  absnegs  28247  n0lts1e0  28368  elnnzs  28401  avglts1d  28453  avglts2d  28454  bdaypw2n0bndlem  28463  z12bdaylem1  28470  lfgrwlkprop  29763  konigsberglem4  30334  frgrwopreglem2  30392  avril1  30542  minvecolem5  30960  minvecolem6  30961  minvecolem7  30962  bcsiALT  31258  pjdifnormii  31762  cvexchi  32448  fldext2chn  33887  ballotlem4  34658  bnj110  35016  wsuclb  36022  dalem18  40009  dalem48  40048  cdlemblem  40121  cdleme7ga  40576  cdlemg27b  41024  sn-inelr  42809  frege116  44287  frege120  44291  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  hoidmv1lelem3  46904  hoidmvlelem3  46908  hoidmvle  46911  257prm  47874  fmtno4prmfac  47885  fmtno4nprmfac193  47887  flsqrt5  47907  139prmALT  47909  31prm  47910  127prm  47912  lighneallem2  47919  stgoldbwt  48089  nnsum3primesle9  48107  wtgoldbnnsum4prm  48115  bgoldbnnsum3prm  48117  lincdifsn  48737  lindslinindsimp1  48770  lindslinindsimp2lem5  48775  lindslinindsimp2  48776  fldivexpfllog2  48878  nnlog2ge0lt1  48879  blen1b  48901  resum2sqorgt0  49022