Theorem breq1i 5154

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

Syntax hints:   ↔ wb 205   = wceq 1542   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  eqbrtri  5168  brtpos0  8213  brtpos  8215  euen1  9022  euen1b  9023  2dom  9026  0sdom1domALT  9235  1sdom2  9236  modom2  9241  1sdomOLD  9245  infglb  9481  infglbb  9482  cnfcom3lem  9694  pr2nelemOLD  9994  axdclem2  10511  rnct  10516  cfpwsdom  10575  inar1  10766  reclem3pr  11040  gt0srpr  11069  mappsrpr  11099  ltpsrpr  11100  map2psrpr  11101  axpre-mulgt0  11159  lt0neg1  11716  le0neg1  11718  reclt1  12105  addltmul  12444  eluz2b1  12899  xlt0neg1  13194  xle0neg1  13196  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  elfznelfzo  13733  bernneq  14188  nn0opthlem1  14224  faclbnd4lem1  14249  hashge0  14343  hashgt23el  14380  hashge2el2difr  14438  cbvsum  15637  divcnvshft  15797  cbvprod  15855  iprodmul  15943  oddge22np1  16288  nn0o1gt2  16320  divalglem1  16333  divalglem6  16337  isprm3  16616  dvdsnprmd  16623  2mulprm  16626  ge2nprmge4  16634  prmgaplem3  16982  isnzr2  20286  chrdvds  21064  chrcong  21065  lindsmm  21367  cpmidpmat  22357  csdfil  23380  iscau3  24777  ioombl1lem4  25060  itg2cn  25263  radcnvlt1  25912  sincosq1sgn  25990  sincosq3sgn  25992  sincosq4sgn  25993  ang180lem3  26296  leibpilem2  26426  issqf  26620  bposlem6  26772  gausslemma2dlem3  26851  nosupinfsep  27215  addscut  27442  mulscut  27568  mulscan2d  27611  recsex  27645  clwlkclwwlklem2  29233  clwlkclwwlk2  29236  clwlkclwwlkf  29241  clwlknf1oclwwlknlem1  29314  konigsberglem5  29489  cvexchi  31600  addltmulALT  31677  xnn01gt  31961  dya2iocct  33217  ballotlemi1  33439  signswch  33510  usgrgt2cycl  34059  cusgracyclt3v  34085  cos2h  36417  tan2h  36418  lhpocnel2  38828  cdlemk19w  39781  lcmineqlem  40855  rencldnfilem  41491  imsqrtvalex  42330  frege70  42617  frege118  42665  hashnzfzclim  43014  dvradcnv2  43039  binomcxplemnotnn0  43048  supxrleubrnmptf  44096  ioonct  44185  fourierdlem112  44869  salexct2  44990  flsqrt5  46197  lighneallem4b  46212  fpprel2  46344  gbegt5  46364  gbowgt5  46365  gbowge7  46366  gbege6  46368  sbgoldbwt  46380  sbgoldbst  46381  sbgoldbalt  46384  sbgoldbm  46387  nnsum3primesle9  46397  nnsum4primesevenALTV  46404  bgoldbtbndlem1  46408  tgblthelfgott  46418  difmodm1lt  47110