Theorem breq2i 5110

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

Syntax hints:   ↔ wb 208   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breqtri  5127  en1  9007  sdom1  9196  enp1i  9225  pm54.43  9961  addclprlem2  10977  map2psrpr  11070  lt0neg2  11696  le0neg2  11698  recgt1  12090  inelr  12187  addltmul  12459  nn0lt2  12638  3halfnz  12654  xlt0neg2  13225  xle0neg2  13227  iccshftr  13492  iccshftl  13494  iccdil  13496  icccntr  13498  hashen1  14385  swrdccatin2  14744  pfxccat3  14749  mertens  15918  aleph1re  16279  dvdslelem  16345  3dvdsdec  16368  3dvds2dec  16369  divalglem5  16433  ndvdsi  16448  bitsfzo  16471  absproddvds  16653  prmfac1  16757  prm23lt5  16852  dec2dvds  17101  dec5dvds2  17103  prmlem0  17143  dprd0  20075  ablfac1lem  20112  minveclem3b  25492  minveclem6  25498  minveclem7  25499  ioombl1lem4  25625  sinhalfpilem  26530  sincosq1lem  26564  sincosq1sgn  26565  sincosq2sgn  26566  sincosq3sgn  26567  sincosq4sgn  26568  bposlem6  27355  gausslemma2dlem1a  27431  2lgsoddprmlem3  27480  nosupinfsep  27798  addcuts  28073  lt0negs2d  28146  mulcut  28227  absnegs  28342  n0lts1e0  28463  elnnzs  28496  avglts1d  28548  avglts2d  28549  bdaypw2n0bndlem  28558  z12bdaylem1  28565  lfgrwlkprop  29888  konigsberglem4  30459  frgrwopreglem2  30517  avril1  30667  minvecolem5  31086  minvecolem6  31087  minvecolem7  31088  bcsiALT  31384  pjdifnormii  31888  cvexchi  32574  fldext2chn  34027  ballotlem4  34798  bnj110  35155  wsuclb  36181  dalem18  40310  dalem48  40349  cdlemblem  40422  cdleme7ga  40877  cdlemg27b  41325  sn-inelr  43114  frege116  44560  frege120  44564  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  hoidmv1lelem3  47172  hoidmvlelem3  47176  hoidmvle  47179  257prm  48175  fmtno4prmfac  48186  fmtno4nprmfac193  48188  flsqrt5  48208  139prmALT  48210  31prm  48211  127prm  48213  lighneallem2  48220  nprmdvdsfacm1lem2  48235  stgoldbwt  48403  nnsum3primesle9  48421  wtgoldbnnsum4prm  48429  bgoldbnnsum3prm  48431  lincdifsn  49051  lindslinindsimp1  49084  lindslinindsimp2lem5  49089  lindslinindsimp2  49090  fldivexpfllog2  49192  nnlog2ge0lt1  49193  blen1b  49215  resum2sqorgt0  49336