Theorem breq1i 5108

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

Syntax hints:   ↔ wb 208   = wceq 1561   class class class wbr 5101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102

This theorem is referenced by:  eqbrtri  5122  brtpos0  8214  brtpos  8216  euen1  9009  euen1b  9010  2dom  9012  0sdom1domALT  9192  1sdom2  9193  modom2  9197  infglb  9438  infglbb  9439  cnfcom3lem  9659  axdclem2  10478  rnct  10483  cfpwsdom  10543  inar1  10734  reclem3pr  11008  gt0srpr  11037  mappsrpr  11067  ltpsrpr  11068  map2psrpr  11069  axpre-mulgt0  11127  lt0neg1  11694  le0neg1  11696  reclt1  12088  addltmul  12458  eluz2b1  12921  xlt0neg1  13223  xle0neg1  13225  iccshftr  13491  iccshftl  13493  iccdil  13495  icccntr  13497  elfznelfzo  13780  bernneq  14243  nn0opthlem1  14282  faclbnd4lem1  14307  hashge0  14401  hashgt23el  14438  hashge2el2difr  14495  cbvsum  15723  divcnvshft  15886  cbvprod  15944  cbvprodv  15945  prodeq1i  15947  iprodmul  16034  oddge22np1  16384  nn0o1gt2  16416  divalglem1  16429  divalglem6  16433  isprm3  16718  dvdsnprmd  16725  2mulprm  16728  ge2nprmge4  16737  prmgaplem3  17090  isnzr2  20569  chrdvds  21579  chrcong  21580  lindsmm  21881  cpmidpmat  22934  csdfil  23955  iscau3  25341  ioombl1lem4  25624  itg2cn  25826  radcnvlt1  26482  sincosq1sgn  26564  sincosq3sgn  26566  sincosq4sgn  26567  ang180lem3  26877  leibpilem2  27007  issqf  27201  bposlem6  27354  gausslemma2dlem3  27433  nosupinfsep  27797  addcuts  28072  mulcut  28226  mulscan2d  28273  recsex  28313  absnegs  28341  avglts1d  28547  avglts2d  28548  z12bdaylem1  28564  z12bday  28579  bdayfin  28581  clwlkclwwlklem2  30203  clwlkclwwlk2  30206  clwlkclwwlkf  30211  clwlknf1oclwwlknlem1  30284  konigsberglem5  30459  cvexchi  32573  addltmulALT  32650  xnn01gt  32973  dya2iocct  34578  ballotlemi1  34801  signswch  34856  usgrgt2cycl  35481  cusgracyclt3v  35507  sumeq2si  36563  prodeq2si  36565  cbvprodvw2  36608  cos2h  38111  tan2h  38112  lhpocnel2  40644  cdlemk19w  41597  lcmineqlem  42670  rencldnfilem  43398  imsqrtvalex  44223  frege70  44510  frege118  44558  hashnzfzclim  44899  dvradcnv2  44924  binomcxplemnotnn0  44933  supxrleubrnmptf  46026  ioonct  46114  fourierdlem112  46793  salexct2  46914  addmodne  47945  m1modnep2mod  47953  difmodm1lt  47960  2timesltsq  47973  2timesltsqm1  47974  flsqrt5  48204  lighneallem4b  48219  fpprel2  48364  gbegt5  48384  gbowgt5  48385  gbowge7  48386  gbege6  48388  sbgoldbwt  48400  sbgoldbst  48401  sbgoldbalt  48404  sbgoldbm  48407  nnsum3primesle9  48417  nnsum4primesevenALTV  48424  bgoldbtbndlem1  48428  tgblthelfgott  48438  gpg3kgrtriexlem5  48710