Theorem breq1i 5155

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

Syntax hints:   ↔ wb 206   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  eqbrtri  5169  brtpos0  8257  brtpos  8259  euen1  9066  euen1b  9067  2dom  9069  0sdom1domALT  9273  1sdom2  9274  modom2  9279  1sdomOLD  9283  infglb  9528  infglbb  9529  cnfcom3lem  9741  pr2nelemOLD  10041  axdclem2  10558  rnct  10563  cfpwsdom  10622  inar1  10813  reclem3pr  11087  gt0srpr  11116  mappsrpr  11146  ltpsrpr  11147  map2psrpr  11148  axpre-mulgt0  11206  lt0neg1  11767  le0neg1  11769  reclt1  12161  addltmul  12500  eluz2b1  12959  xlt0neg1  13258  xle0neg1  13260  iccshftr  13523  iccshftl  13525  iccdil  13527  icccntr  13529  elfznelfzo  13808  bernneq  14265  nn0opthlem1  14304  faclbnd4lem1  14329  hashge0  14423  hashgt23el  14460  hashge2el2difr  14517  cbvsum  15728  divcnvshft  15888  cbvprod  15946  cbvprodv  15947  prodeq1i  15949  iprodmul  16036  oddge22np1  16383  nn0o1gt2  16415  divalglem1  16428  divalglem6  16432  isprm3  16717  dvdsnprmd  16724  2mulprm  16727  ge2nprmge4  16735  prmgaplem3  17087  isnzr2  20535  chrdvds  21559  chrcong  21560  lindsmm  21866  cpmidpmat  22895  csdfil  23918  iscau3  25326  ioombl1lem4  25610  itg2cn  25813  radcnvlt1  26476  sincosq1sgn  26555  sincosq3sgn  26557  sincosq4sgn  26558  ang180lem3  26869  leibpilem2  26999  issqf  27194  bposlem6  27348  gausslemma2dlem3  27427  nosupinfsep  27792  addscut  28026  mulscut  28173  mulscan2d  28220  recsex  28258  abssneg  28286  clwlkclwwlklem2  30029  clwlkclwwlk2  30032  clwlkclwwlkf  30037  clwlknf1oclwwlknlem1  30110  konigsberglem5  30285  cvexchi  32398  addltmulALT  32475  xnn01gt  32781  dya2iocct  34262  ballotlemi1  34484  signswch  34555  usgrgt2cycl  35115  cusgracyclt3v  35141  sumeq2si  36184  prodeq2si  36186  cbvprodvw2  36230  cos2h  37598  tan2h  37599  lhpocnel2  40002  cdlemk19w  40955  lcmineqlem  42034  rencldnfilem  42808  imsqrtvalex  43636  frege70  43923  frege118  43971  hashnzfzclim  44318  dvradcnv2  44343  binomcxplemnotnn0  44352  supxrleubrnmptf  45401  ioonct  45490  fourierdlem112  46174  salexct2  46295  addmodne  47284  m1modnep2mod  47292  flsqrt5  47519  lighneallem4b  47534  fpprel2  47666  gbegt5  47686  gbowgt5  47687  gbowge7  47688  gbege6  47690  sbgoldbwt  47702  sbgoldbst  47703  sbgoldbalt  47706  sbgoldbm  47709  nnsum3primesle9  47719  nnsum4primesevenALTV  47726  bgoldbtbndlem1  47730  tgblthelfgott  47740  difmodm1lt  48372