Theorem breq2i 5093

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breqtri  5110  en1  8971  sdom1  9160  enp1i  9189  pm54.43  9925  addclprlem2  10940  map2psrpr  11033  lt0neg2  11657  le0neg2  11659  recgt1  12052  inelr  12149  addltmul  12413  nn0lt2  12592  3halfnz  12608  xlt0neg2  13172  xle0neg2  13174  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  hashen1  14332  swrdccatin2  14691  pfxccat3  14696  mertens  15851  aleph1re  16212  dvdslelem  16278  3dvdsdec  16301  3dvds2dec  16302  divalglem5  16366  ndvdsi  16381  bitsfzo  16404  absproddvds  16586  prmfac1  16690  prm23lt5  16785  dec2dvds  17034  dec5dvds2  17036  prmlem0  17076  dprd0  20008  ablfac1lem  20045  minveclem3b  25395  minveclem6  25401  minveclem7  25402  ioombl1lem4  25528  sinhalfpilem  26427  sincosq1lem  26461  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  bposlem6  27252  gausslemma2dlem1a  27328  2lgsoddprmlem3  27377  nosupinfsep  27696  addcuts  27970  lt0negs2d  28043  mulcut  28124  absnegs  28239  n0lts1e0  28360  elnnzs  28393  avglts1d  28445  avglts2d  28446  bdaypw2n0bndlem  28455  z12bdaylem1  28462  lfgrwlkprop  29754  konigsberglem4  30325  frgrwopreglem2  30383  avril1  30533  minvecolem5  30952  minvecolem6  30953  minvecolem7  30954  bcsiALT  31250  pjdifnormii  31754  cvexchi  32440  fldext2chn  33872  ballotlem4  34643  bnj110  35000  wsuclb  36008  dalem18  40127  dalem48  40166  cdlemblem  40239  cdleme7ga  40694  cdlemg27b  41142  sn-inelr  42932  frege116  44406  frege120  44410  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  hoidmv1lelem3  47021  hoidmvlelem3  47025  hoidmvle  47028  257prm  48024  fmtno4prmfac  48035  fmtno4nprmfac193  48037  flsqrt5  48057  139prmALT  48059  31prm  48060  127prm  48062  lighneallem2  48069  nprmdvdsfacm1lem2  48084  stgoldbwt  48252  nnsum3primesle9  48270  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  lincdifsn  48900  lindslinindsimp1  48933  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  fldivexpfllog2  49041  nnlog2ge0lt1  49042  blen1b  49064  resum2sqorgt0  49185