Theorem breq2i 5038

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

Syntax hints:   ↔ wb 209   = wceq 1542   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031

This theorem is referenced by:  breqtri  5055  en1  8623  snnen2o  8757  enp1i  8830  pm54.43  9503  addclprlem2  10517  map2psrpr  10610  lt0neg2  11225  le0neg2  11227  recgt1  11614  addltmul  11952  nn0lt2  12126  3halfnz  12142  xlt0neg2  12696  xle0neg2  12698  iccshftr  12960  iccshftl  12962  iccdil  12964  icccntr  12966  hashen1  13823  swrdccatin2  14180  pfxccat3  14185  mertens  15334  aleph1re  15690  dvdslelem  15754  3dvdsdec  15777  3dvds2dec  15778  divalglem5  15842  ndvdsi  15857  bitsfzo  15878  absproddvds  16058  prmfac1  16162  prm23lt5  16251  dec2dvds  16499  dec5dvds2  16501  prmlem0  16542  dprd0  19272  ablfac1lem  19309  minveclem3b  24180  minveclem6  24186  minveclem7  24187  ioombl1lem4  24313  sinhalfpilem  25208  sincosq1lem  25242  sincosq1sgn  25243  sincosq2sgn  25244  sincosq3sgn  25245  sincosq4sgn  25246  bposlem6  26025  gausslemma2dlem1a  26101  2lgsoddprmlem3  26150  lfgrwlkprop  27629  konigsberglem4  28192  frgrwopreglem2  28250  avril1  28400  minvecolem5  28816  minvecolem6  28817  minvecolem7  28818  bcsiALT  29114  pjdifnormii  29618  cvexchi  30304  ballotlem4  32035  bnj110  32409  wsuclb  33433  nosupinfsep  33576  dalem18  37318  dalem48  37357  cdlemblem  37430  cdleme7ga  37885  cdlemg27b  38333  frege116  41133  frege120  41137  ioodvbdlimc1lem2  43015  ioodvbdlimc2lem  43017  hoidmv1lelem3  43673  hoidmvlelem3  43677  hoidmvle  43680  257prm  44547  fmtno4prmfac  44558  fmtno4nprmfac193  44560  flsqrt5  44580  139prmALT  44582  31prm  44583  127prm  44585  lighneallem2  44592  stgoldbwt  44762  nnsum3primesle9  44780  wtgoldbnnsum4prm  44788  bgoldbnnsum3prm  44790  lincdifsn  45299  lindslinindsimp1  45332  lindslinindsimp2lem5  45337  lindslinindsimp2  45338  fldivexpfllog2  45445  nnlog2ge0lt1  45446  blen1b  45468  resum2sqorgt0  45589