Theorem breq2i 5111

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqtri  5130  en1  9037  sdom1  9227  enp1i  9256  pm54.43  10031  addclprlem2  11051  map2psrpr  11144  lt0neg2  11770  le0neg2  11772  recgt1  12160  inelr  12257  addltmul  12529  nn0lt2  12709  3halfnz  12725  xlt0neg2  13297  xle0neg2  13299  iccshftr  13564  iccshftl  13566  iccdil  13568  icccntr  13570  hashen1  14459  swrdccatin2  14823  pfxccat3  14828  mertens  16000  aleph1re  16358  dvdslelem  16424  3dvdsdec  16447  3dvds2dec  16448  divalglem5  16512  ndvdsi  16527  bitsfzo  16550  absproddvds  16732  prmfac1  16836  prm23lt5  16931  dec2dvds  17180  dec5dvds2  17182  prmlem0  17222  dprd0  20186  ablfac1lem  20223  minveclem3b  25688  minveclem6  25694  minveclem7  25695  ioombl1lem4  25821  sinhalfpilem  26733  sincosq1lem  26767  sincosq1sgn  26768  sincosq2sgn  26769  sincosq3sgn  26770  sincosq4sgn  26771  bposlem6  27557  gausslemma2dlem1a  27633  2lgsoddprmlem3  27682  nosupinfsep  28000  addcuts  28275  lt0negs2d  28348  mulcut  28429  absnegs  28544  n0lts1e0  28665  elnnzs  28698  avglts1d  28750  avglts2d  28751  bdaypw2n0bndlem  28760  z12bdaylem1  28767  lfgrwlkprop  30181  konigsberglem4  30767  frgrwopreglem2  30825  avril1  30975  minvecolem5  31394  minvecolem6  31395  minvecolem7  31396  bcsiALT  31692  pjdifnormii  32196  cvexchi  32882  fldext2chn  34271  ballotlem4  35043  bnj110  35400  wsuclb  36488  dalem18  40619  dalem48  40658  cdlemblem  40731  cdleme7ga  41186  cdlemg27b  41634  sn-inelr  43440  frege116  44884  frege120  44888  ioodvbdlimc1lem2  46825  ioodvbdlimc2lem  46827  hoidmv1lelem3  47486  hoidmvlelem3  47490  hoidmvle  47493  257prm  48529  fmtno4prmfac  48540  fmtno4nprmfac193  48542  flsqrt5  48562  139prmALT  48564  31prm  48565  127prm  48567  lighneallem2  48574  nprmdvdsfacm1lem2  48589  stgoldbwt  48757  nnsum3primesle9  48775  wtgoldbnnsum4prm  48783  bgoldbnnsum3prm  48785  lincdifsn  49419  lindslinindsimp1  49452  lindslinindsimp2lem5  49457  lindslinindsimp2  49458  fldivexpfllog2  49560  nnlog2ge0lt1  49561  blen1b  49583  resum2sqorgt0  49704