Theorem breq1i 5034

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

Syntax hints:   ↔ wb 209   = wceq 1542   class class class wbr 5027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028

This theorem is referenced by:  eqbrtri  5048  brtpos0  7921  brtpos  7923  euen1  8619  euen1b  8620  2dom  8622  0sdom1dom  8788  modom2  8792  1sdom  8793  infglb  9020  infglbb  9021  cnfcom3lem  9232  pr2nelem  9497  axdclem2  10013  rnct  10018  cfpwsdom  10077  inar1  10268  reclem3pr  10542  gt0srpr  10571  mappsrpr  10601  ltpsrpr  10602  map2psrpr  10603  axpre-mulgt0  10661  lt0neg1  11217  le0neg1  11219  reclt1  11606  addltmul  11945  eluz2b1  12394  xlt0neg1  12688  xle0neg1  12690  iccshftr  12953  iccshftl  12955  iccdil  12957  icccntr  12959  elfznelfzo  13226  bernneq  13675  nn0opthlem1  13713  faclbnd4lem1  13738  hashge0  13833  hashgt23el  13870  hashge2el2difr  13926  cbvsum  15138  divcnvshft  15296  cbvprod  15354  iprodmul  15442  oddge22np1  15787  nn0o1gt2  15819  divalglem1  15832  divalglem6  15836  isprm3  16117  dvdsnprmd  16124  2mulprm  16127  ge2nprmge4  16135  prmgaplem3  16482  isnzr2  20148  chrdvds  20340  chrcong  20341  lindsmm  20637  cpmidpmat  21617  csdfil  22638  iscau3  24023  ioombl1lem4  24306  itg2cn  24508  radcnvlt1  25157  sincosq1sgn  25235  sincosq3sgn  25237  sincosq4sgn  25238  ang180lem3  25541  leibpilem2  25671  issqf  25865  bposlem6  26017  gausslemma2dlem3  26096  clwlkclwwlklem2  27929  clwlkclwwlk2  27932  clwlkclwwlkf  27937  clwlknf1oclwwlknlem1  28010  konigsberglem5  28185  cvexchi  30296  addltmulALT  30373  xnn01gt  30660  dya2iocct  31809  ballotlemi1  32031  signswch  32102  usgrgt2cycl  32655  cusgracyclt3v  32681  nosupinfsep  33568  cos2h  35380  tan2h  35381  lhpocnel2  37645  cdlemk19w  38598  lcmineqlem  39669  rencldnfilem  40198  imsqrtvalex  40783  frege70  41071  frege118  41119  hashnzfzclim  41462  dvradcnv2  41487  binomcxplemnotnn0  41496  supxrleubrnmptf  42515  ioonct  42599  fourierdlem112  43285  salexct2  43404  flsqrt5  44564  lighneallem4b  44579  fpprel2  44711  gbegt5  44731  gbowgt5  44732  gbowge7  44733  gbege6  44735  sbgoldbwt  44747  sbgoldbst  44748  sbgoldbalt  44751  sbgoldbm  44754  nnsum3primesle9  44764  nnsum4primesevenALTV  44771  bgoldbtbndlem1  44775  tgblthelfgott  44785  difmodm1lt  45386