Theorem breq1i 5037

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
breq1i	⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq1 5033	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 209   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  eqbrtri  5051  brtpos0  7882  brtpos  7884  euen1  8562  euen1b  8563  2dom  8565  0sdom1dom  8700  modom2  8704  1sdom  8705  infglb  8938  infglbb  8939  cnfcom3lem  9150  pr2nelem  9415  axdclem2  9931  rnct  9936  cfpwsdom  9995  inar1  10186  reclem3pr  10460  gt0srpr  10489  mappsrpr  10519  ltpsrpr  10520  map2psrpr  10521  axpre-mulgt0  10579  lt0neg1  11135  le0neg1  11137  reclt1  11524  addltmul  11861  eluz2b1  12307  xlt0neg1  12600  xle0neg1  12602  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  elfznelfzo  13137  bernneq  13586  nn0opthlem1  13624  faclbnd4lem1  13649  hashge0  13744  hashgt23el  13781  hashge2el2difr  13835  cbvsum  15044  divcnvshft  15202  cbvprod  15261  iprodmul  15349  oddge22np1  15690  nn0o1gt2  15722  divalglem1  15735  divalglem6  15739  isprm3  16017  dvdsnprmd  16024  2mulprm  16027  ge2nprmge4  16035  prmgaplem3  16379  isnzr2  20029  chrdvds  20220  chrcong  20221  lindsmm  20517  cpmidpmat  21478  csdfil  22499  iscau3  23882  ioombl1lem4  24165  itg2cn  24367  radcnvlt1  25013  sincosq1sgn  25091  sincosq3sgn  25093  sincosq4sgn  25094  ang180lem3  25397  leibpilem2  25527  issqf  25721  bposlem6  25873  gausslemma2dlem3  25952  clwlkclwwlklem2  27785  clwlkclwwlk2  27788  clwlkclwwlkf  27793  clwlknf1oclwwlknlem1  27866  konigsberglem5  28041  cvexchi  30152  addltmulALT  30229  xnn01gt  30521  dya2iocct  31648  ballotlemi1  31870  signswch  31941  usgrgt2cycl  32490  cusgracyclt3v  32516  cos2h  35048  tan2h  35049  lhpocnel2  37315  cdlemk19w  38268  lcmineqlem  39340  rencldnfilem  39761  imsqrtvalex  40346  frege70  40634  frege118  40682  hashnzfzclim  41026  dvradcnv2  41051  binomcxplemnotnn0  41060  supxrleubrnmptf  42090  ioonct  42174  fourierdlem112  42860  salexct2  42979  flsqrt5  44111  lighneallem4b  44127  fpprel2  44259  gbegt5  44279  gbowgt5  44280  gbowge7  44281  gbege6  44283  sbgoldbwt  44295  sbgoldbst  44296  sbgoldbalt  44299  sbgoldbm  44302  nnsum3primesle9  44312  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  tgblthelfgott  44333  difmodm1lt  44936