Theorem breq2i 5117

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is used by:  breqtri  5136  en1  9017  sdom1  9206  enp1i  9235  pm54.43  9992  addclprlem2  11006  map2psrpr  11099  lt0neg2  11725  le0neg2  11727  recgt1  12115  inelr  12212  addltmul  12484  nn0lt2  12663  3halfnz  12679  xlt0neg2  13250  xle0neg2  13252  iccshftr  13517  iccshftl  13519  iccdil  13521  icccntr  13523  hashen1  14411  swrdccatin2  14771  pfxccat3  14776  mertens  15945  aleph1re  16305  dvdslelem  16371  3dvdsdec  16394  3dvds2dec  16395  divalglem5  16459  ndvdsi  16474  bitsfzo  16497  absproddvds  16679  prmfac1  16783  prm23lt5  16878  dec2dvds  17127  dec5dvds2  17129  prmlem0  17169  dprd0  20107  ablfac1lem  20144  minveclem3b  25596  minveclem6  25602  minveclem7  25603  ioombl1lem4  25729  sinhalfpilem  26637  sincosq1lem  26671  sincosq1sgn  26672  sincosq2sgn  26673  sincosq3sgn  26674  sincosq4sgn  26675  bposlem6  27462  gausslemma2dlem1a  27538  2lgsoddprmlem3  27587  nosupinfsep  27905  addcuts  28180  lt0negs2d  28253  mulcut  28334  absnegs  28449  n0lts1e0  28570  elnnzs  28603  avglts1d  28655  avglts2d  28656  bdaypw2n0bndlem  28665  z12bdaylem1  28672  lfgrwlkprop  30044  konigsberglem4  30615  frgrwopreglem2  30673  avril1  30823  minvecolem5  31242  minvecolem6  31243  minvecolem7  31244  bcsiALT  31540  pjdifnormii  32044  cvexchi  32730  fldext2chn  34127  ballotlem4  34898  bnj110  35255  wsuclb  36326  dalem18  40483  dalem48  40522  cdlemblem  40595  cdleme7ga  41050  cdlemg27b  41498  sn-inelr  43289  frege116  44733  frege120  44737  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  hoidmv1lelem3  47335  hoidmvlelem3  47339  hoidmvle  47342  257prm  48341  fmtno4prmfac  48352  fmtno4nprmfac193  48354  flsqrt5  48374  139prmALT  48376  31prm  48377  127prm  48379  lighneallem2  48386  nprmdvdsfacm1lem2  48401  stgoldbwt  48569  nnsum3primesle9  48587  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  lincdifsn  49232  lindslinindsimp1  49265  lindslinindsimp2lem5  49270  lindslinindsimp2  49271  fldivexpfllog2  49373  nnlog2ge0lt1  49374  blen1b  49396  resum2sqorgt0  49517