Theorem breq2i 5110

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breqtri  5129  en1  9051  sdom1  9241  enp1i  9270  pm54.43  10082  addclprlem2  11102  map2psrpr  11195  lt0neg2  11823  le0neg2  11825  recgt1  12213  inelr  12310  addltmul  12582  nn0lt2  12762  3halfnz  12778  xlt0neg2  13350  xle0neg2  13352  iccshftr  13617  iccshftl  13619  iccdil  13621  icccntr  13623  hashen1  14514  swrdccatin2  14878  pfxccat3  14883  mertens  16055  aleph1re  16413  dvdslelem  16479  3dvdsdec  16502  3dvds2dec  16503  divalglem5  16567  ndvdsi  16582  bitsfzo  16605  absproddvds  16792  prmfac1  16896  prm23lt5  16992  dec2dvds  17241  dec5dvds2  17243  prmlem0  17283  dprd0  20247  ablfac1lem  20284  minveclem3b  25749  minveclem6  25755  minveclem7  25756  ioombl1lem4  25882  sinhalfpilem  26792  sincosq1lem  26826  sincosq1sgn  26827  sincosq2sgn  26828  sincosq3sgn  26829  sincosq4sgn  26830  bposlem6  27616  gausslemma2dlem1a  27692  2lgsoddprmlem3  27741  nosupinfsep  28089  addcuts  28364  lt0negs2d  28437  mulcut  28518  absnegs  28633  n0lts1e0  28754  elnnzs  28787  avglts1d  28839  avglts2d  28840  bdaypw2n0bndlem  28849  z12bdaylem1  28856  lfgrwlkprop  30270  konigsberglem4  30856  frgrwopreglem2  30914  avril1  31064  minvecolem5  31483  minvecolem6  31484  minvecolem7  31485  bcsiALT  31781  pjdifnormii  32285  cvexchi  32971  fldext2chn  34360  ballotlem4  35131  bnj110  35488  wsuclb  36590  dalem18  40739  dalem48  40778  cdlemblem  40851  cdleme7ga  41306  cdlemg27b  41754  sn-inelr  43552  frege116  44979  frege120  44983  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  hoidmv1lelem3  47603  hoidmvlelem3  47607  hoidmvle  47610  257prm  48646  fmtno4prmfac  48657  fmtno4nprmfac193  48659  flsqrt5  48679  139prmALT  48681  31prm  48682  127prm  48684  lighneallem2  48691  nprmdvdsfacm1lem2  48706  stgoldbwt  48874  nnsum3primesle9  48892  wtgoldbnnsum4prm  48900  bgoldbnnsum3prm  48902  lincdifsn  49536  lindslinindsimp1  49569  lindslinindsimp2lem5  49574  lindslinindsimp2  49575  fldivexpfllog2  49677  nnlog2ge0lt1  49678  blen1b  49700  resum2sqorgt0  49821