Theorem breq2i 5119

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

Syntax hints:   ↔ wb 209   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  breqtri  5138  en1  9021  sdom1  9210  enp1i  9239  pm54.43  9987  addclprlem2  11002  map2psrpr  11095  lt0neg2  11721  le0neg2  11723  recgt1  12111  inelr  12208  addltmul  12480  nn0lt2  12659  3halfnz  12675  xlt0neg2  13246  xle0neg2  13248  iccshftr  13513  iccshftl  13515  iccdil  13517  icccntr  13519  hashen1  14406  swrdccatin2  14766  pfxccat3  14771  mertens  15940  aleph1re  16301  dvdslelem  16367  3dvdsdec  16390  3dvds2dec  16391  divalglem5  16455  ndvdsi  16470  bitsfzo  16493  absproddvds  16675  prmfac1  16779  prm23lt5  16874  dec2dvds  17123  dec5dvds2  17125  prmlem0  17165  dprd0  20103  ablfac1lem  20140  minveclem3b  25556  minveclem6  25562  minveclem7  25563  ioombl1lem4  25689  sinhalfpilem  26594  sincosq1lem  26628  sincosq1sgn  26629  sincosq2sgn  26630  sincosq3sgn  26631  sincosq4sgn  26632  bposlem6  27419  gausslemma2dlem1a  27495  2lgsoddprmlem3  27544  nosupinfsep  27862  addcuts  28137  lt0negs2d  28210  mulcut  28291  absnegs  28406  n0lts1e0  28527  elnnzs  28560  avglts1d  28612  avglts2d  28613  bdaypw2n0bndlem  28622  z12bdaylem1  28629  lfgrwlkprop  29976  konigsberglem4  30547  frgrwopreglem2  30605  avril1  30755  minvecolem5  31174  minvecolem6  31175  minvecolem7  31176  bcsiALT  31472  pjdifnormii  31976  cvexchi  32662  fldext2chn  34063  ballotlem4  34834  bnj110  35191  wsuclb  36251  dalem18  40380  dalem48  40419  cdlemblem  40492  cdleme7ga  40947  cdlemg27b  41395  sn-inelr  43186  frege116  44632  frege120  44636  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  hoidmv1lelem3  47234  hoidmvlelem3  47238  hoidmvle  47241  257prm  48237  fmtno4prmfac  48248  fmtno4nprmfac193  48250  flsqrt5  48270  139prmALT  48272  31prm  48273  127prm  48275  lighneallem2  48282  nprmdvdsfacm1lem2  48297  stgoldbwt  48465  nnsum3primesle9  48483  wtgoldbnnsum4prm  48491  bgoldbnnsum3prm  48493  lincdifsn  49124  lindslinindsimp1  49157  lindslinindsimp2lem5  49162  lindslinindsimp2  49163  fldivexpfllog2  49265  nnlog2ge0lt1  49266  blen1b  49288  resum2sqorgt0  49409