Theorem breq2i 5115

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breqtri  5134  en1  9033  sdom1  9223  enp1i  9252  pm54.43  10009  addclprlem2  11027  map2psrpr  11120  lt0neg2  11746  le0neg2  11748  recgt1  12136  inelr  12233  addltmul  12505  nn0lt2  12685  3halfnz  12701  xlt0neg2  13272  xle0neg2  13274  iccshftr  13539  iccshftl  13541  iccdil  13543  icccntr  13545  hashen1  14434  swrdccatin2  14798  pfxccat3  14803  mertens  15975  aleph1re  16335  dvdslelem  16401  3dvdsdec  16424  3dvds2dec  16425  divalglem5  16489  ndvdsi  16504  bitsfzo  16527  absproddvds  16709  prmfac1  16813  prm23lt5  16908  dec2dvds  17157  dec5dvds2  17159  prmlem0  17199  dprd0  20159  ablfac1lem  20196  minveclem3b  25655  minveclem6  25661  minveclem7  25662  ioombl1lem4  25788  sinhalfpilem  26696  sincosq1lem  26730  sincosq1sgn  26731  sincosq2sgn  26732  sincosq3sgn  26733  sincosq4sgn  26734  bposlem6  27521  gausslemma2dlem1a  27597  2lgsoddprmlem3  27646  nosupinfsep  27964  addcuts  28239  lt0negs2d  28312  mulcut  28393  absnegs  28508  n0lts1e0  28629  elnnzs  28662  avglts1d  28714  avglts2d  28715  bdaypw2n0bndlem  28724  z12bdaylem1  28731  lfgrwlkprop  30133  konigsberglem4  30719  frgrwopreglem2  30777  avril1  30927  minvecolem5  31346  minvecolem6  31347  minvecolem7  31348  bcsiALT  31644  pjdifnormii  32148  cvexchi  32834  fldext2chn  34223  ballotlem4  34995  bnj110  35352  wsuclb  36390  dalem18  40539  dalem48  40578  cdlemblem  40651  cdleme7ga  41106  cdlemg27b  41554  sn-inelr  43360  frege116  44804  frege120  44808  ioodvbdlimc1lem2  46745  ioodvbdlimc2lem  46747  hoidmv1lelem3  47406  hoidmvlelem3  47410  hoidmvle  47413  257prm  48449  fmtno4prmfac  48460  fmtno4nprmfac193  48462  flsqrt5  48482  139prmALT  48484  31prm  48485  127prm  48487  lighneallem2  48494  nprmdvdsfacm1lem2  48509  stgoldbwt  48677  nnsum3primesle9  48695  wtgoldbnnsum4prm  48703  bgoldbnnsum3prm  48705  lincdifsn  49339  lindslinindsimp1  49372  lindslinindsimp2lem5  49377  lindslinindsimp2  49378  fldivexpfllog2  49480  nnlog2ge0lt1  49481  blen1b  49503  resum2sqorgt0  49624