Theorem breq2i 5140

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

Syntax hints:   ↔ wb 205   = wceq 1541   class class class wbr 5132

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3426  df-v 3468  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-nul 4310  df-if 4514  df-sn 4614  df-pr 4616  df-op 4620  df-br 5133

This theorem is referenced by:  breqtri  5157  en1  8994  en1OLD  8995  snnen2oOLD  9200  sdom1  9215  enp1i  9252  enp1iOLD  9253  pm54.43  9968  addclprlem2  10984  map2psrpr  11077  lt0neg2  11693  le0neg2  11695  recgt1  12082  addltmul  12420  nn0lt2  12597  3halfnz  12613  xlt0neg2  13171  xle0neg2  13173  iccshftr  13435  iccshftl  13437  iccdil  13439  icccntr  13441  hashen1  14302  swrdccatin2  14651  pfxccat3  14656  mertens  15804  aleph1re  16160  dvdslelem  16224  3dvdsdec  16247  3dvds2dec  16248  divalglem5  16312  ndvdsi  16327  bitsfzo  16348  absproddvds  16526  prmfac1  16630  prm23lt5  16719  dec2dvds  16968  dec5dvds2  16970  prmlem0  17011  dprd0  19846  ablfac1lem  19883  minveclem3b  24851  minveclem6  24857  minveclem7  24858  ioombl1lem4  24984  sinhalfpilem  25879  sincosq1lem  25913  sincosq1sgn  25914  sincosq2sgn  25915  sincosq3sgn  25916  sincosq4sgn  25917  bposlem6  26696  gausslemma2dlem1a  26772  2lgsoddprmlem3  26821  nosupinfsep  27139  lfgrwlkprop  28739  konigsberglem4  29303  frgrwopreglem2  29361  avril1  29511  minvecolem5  29927  minvecolem6  29928  minvecolem7  29929  bcsiALT  30225  pjdifnormii  30729  cvexchi  31415  ballotlem4  33228  bnj110  33600  wsuclb  34530  dalem18  38257  dalem48  38296  cdlemblem  38369  cdleme7ga  38824  cdlemg27b  39272  frege116  42413  frege120  42417  ioodvbdlimc1lem2  44333  ioodvbdlimc2lem  44335  hoidmv1lelem3  44994  hoidmvlelem3  44998  hoidmvle  45001  257prm  45913  fmtno4prmfac  45924  fmtno4nprmfac193  45926  flsqrt5  45946  139prmALT  45948  31prm  45949  127prm  45951  lighneallem2  45958  stgoldbwt  46128  nnsum3primesle9  46146  wtgoldbnnsum4prm  46154  bgoldbnnsum3prm  46156  lincdifsn  46665  lindslinindsimp1  46698  lindslinindsimp2lem5  46703  lindslinindsimp2  46704  fldivexpfllog2  46811  nnlog2ge0lt1  46812  blen1b  46834  resum2sqorgt0  46955