Theorem breq2i 5100

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breqtri  5117  en1  8949  sdom1  9139  enp1i  9168  pm54.43  9897  addclprlem2  10911  map2psrpr  11004  lt0neg2  11627  le0neg2  11629  recgt1  12021  inelr  12118  addltmul  12360  nn0lt2  12539  3halfnz  12555  xlt0neg2  13122  xle0neg2  13124  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  hashen1  14277  swrdccatin2  14635  pfxccat3  14640  mertens  15793  aleph1re  16154  dvdslelem  16220  3dvdsdec  16243  3dvds2dec  16244  divalglem5  16308  ndvdsi  16323  bitsfzo  16346  absproddvds  16528  prmfac1  16631  prm23lt5  16726  dec2dvds  16975  dec5dvds2  16977  prmlem0  17017  dprd0  19912  ablfac1lem  19949  minveclem3b  25326  minveclem6  25332  minveclem7  25333  ioombl1lem4  25460  sinhalfpilem  26370  sincosq1lem  26404  sincosq1sgn  26405  sincosq2sgn  26406  sincosq3sgn  26407  sincosq4sgn  26408  bposlem6  27198  gausslemma2dlem1a  27274  2lgsoddprmlem3  27323  nosupinfsep  27642  addscut  27890  slt0neg2d  27962  mulscut  28040  abssneg  28154  elnnzs  28294  avgslt1d  28344  avgslt2d  28345  lfgrwlkprop  29631  konigsberglem4  30199  frgrwopreglem2  30257  avril1  30407  minvecolem5  30825  minvecolem6  30826  minvecolem7  30827  bcsiALT  31123  pjdifnormii  31627  cvexchi  32313  fldext2chn  33701  ballotlem4  34473  bnj110  34831  wsuclb  35812  dalem18  39670  dalem48  39709  cdlemblem  39782  cdleme7ga  40237  cdlemg27b  40685  sn-inelr  42470  frege116  43962  frege120  43966  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  hoidmv1lelem3  46584  hoidmvlelem3  46588  hoidmvle  46591  257prm  47555  fmtno4prmfac  47566  fmtno4nprmfac193  47568  flsqrt5  47588  139prmALT  47590  31prm  47591  127prm  47593  lighneallem2  47600  stgoldbwt  47770  nnsum3primesle9  47788  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  lincdifsn  48419  lindslinindsimp1  48452  lindslinindsimp2lem5  48457  lindslinindsimp2  48458  fldivexpfllog2  48560  nnlog2ge0lt1  48561  blen1b  48583  resum2sqorgt0  48704