Theorem breq2i 5083

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

Syntax hints:   ↔ wb 208   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  breqtri  5100  en1  8965  sdom1  9154  enp1i  9183  pm54.43  9920  addclprlem2  10935  map2psrpr  11028  lt0neg2  11652  le0neg2  11654  recgt1  12047  inelr  12144  addltmul  12408  nn0lt2  12587  3halfnz  12603  xlt0neg2  13167  xle0neg2  13169  iccshftr  13434  iccshftl  13436  iccdil  13438  icccntr  13440  hashen1  14327  swrdccatin2  14686  pfxccat3  14691  mertens  15846  aleph1re  16207  dvdslelem  16273  3dvdsdec  16296  3dvds2dec  16297  divalglem5  16361  ndvdsi  16376  bitsfzo  16399  absproddvds  16581  prmfac1  16685  prm23lt5  16780  dec2dvds  17029  dec5dvds2  17031  prmlem0  17071  dprd0  20003  ablfac1lem  20040  minveclem3b  25417  minveclem6  25423  minveclem7  25424  ioombl1lem4  25550  sinhalfpilem  26449  sincosq1lem  26483  sincosq1sgn  26484  sincosq2sgn  26485  sincosq3sgn  26486  sincosq4sgn  26487  bposlem6  27274  gausslemma2dlem1a  27350  2lgsoddprmlem3  27399  nosupinfsep  27718  addcuts  27992  lt0negs2d  28065  mulcut  28146  absnegs  28261  n0lts1e0  28382  elnnzs  28415  avglts1d  28467  avglts2d  28468  bdaypw2n0bndlem  28477  z12bdaylem1  28484  lfgrwlkprop  29776  konigsberglem4  30347  frgrwopreglem2  30405  avril1  30555  minvecolem5  30974  minvecolem6  30975  minvecolem7  30976  bcsiALT  31272  pjdifnormii  31776  cvexchi  32462  fldext2chn  33924  ballotlem4  34695  bnj110  35055  wsuclb  36069  dalem18  40188  dalem48  40227  cdlemblem  40300  cdleme7ga  40755  cdlemg27b  41203  sn-inelr  42992  frege116  44438  frege120  44442  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  hoidmv1lelem3  47050  hoidmvlelem3  47054  hoidmvle  47057  257prm  48053  fmtno4prmfac  48064  fmtno4nprmfac193  48066  flsqrt5  48086  139prmALT  48088  31prm  48089  127prm  48091  lighneallem2  48098  nprmdvdsfacm1lem2  48113  stgoldbwt  48281  nnsum3primesle9  48299  wtgoldbnnsum4prm  48307  bgoldbnnsum3prm  48309  lincdifsn  48929  lindslinindsimp1  48962  lindslinindsimp2lem5  48967  lindslinindsimp2  48968  fldivexpfllog2  49070  nnlog2ge0lt1  49071  blen1b  49093  resum2sqorgt0  49214