Theorem breq1i 5093

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5086

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtri  5107  brtpos0  8177  brtpos  8179  euen1  8968  euen1b  8969  2dom  8971  0sdom1domALT  9151  1sdom2  9152  modom2  9156  infglb  9398  infglbb  9399  cnfcom3lem  9618  axdclem2  10436  rnct  10441  cfpwsdom  10501  inar1  10692  reclem3pr  10966  gt0srpr  10995  mappsrpr  11025  ltpsrpr  11026  map2psrpr  11027  axpre-mulgt0  11085  lt0neg1  11650  le0neg1  11652  reclt1  12045  addltmul  12407  eluz2b1  12863  xlt0neg1  13165  xle0neg1  13167  iccshftr  13433  iccshftl  13435  iccdil  13437  icccntr  13439  elfznelfzo  13722  bernneq  14185  nn0opthlem1  14224  faclbnd4lem1  14249  hashge0  14343  hashgt23el  14380  hashge2el2difr  14437  cbvsum  15651  divcnvshft  15814  cbvprod  15872  cbvprodv  15873  prodeq1i  15875  iprodmul  15962  oddge22np1  16312  nn0o1gt2  16344  divalglem1  16357  divalglem6  16361  isprm3  16646  dvdsnprmd  16653  2mulprm  16656  ge2nprmge4  16665  prmgaplem3  17018  isnzr2  20489  chrdvds  21519  chrcong  21520  lindsmm  21821  cpmidpmat  22851  csdfil  23872  iscau3  25258  ioombl1lem4  25541  itg2cn  25743  radcnvlt1  26399  sincosq1sgn  26478  sincosq3sgn  26480  sincosq4sgn  26481  ang180lem3  26791  leibpilem2  26921  issqf  27116  bposlem6  27269  gausslemma2dlem3  27348  nosupinfsep  27713  addcuts  27987  mulcut  28141  mulscan2d  28188  recsex  28228  absnegs  28256  avglts1d  28462  avglts2d  28463  z12bdaylem1  28479  z12bday  28494  bdayfin  28496  clwlkclwwlklem2  30088  clwlkclwwlk2  30091  clwlkclwwlkf  30096  clwlknf1oclwwlknlem1  30169  konigsberglem5  30344  cvexchi  32458  addltmulALT  32535  xnn01gt  32861  dya2iocct  34443  ballotlemi1  34666  signswch  34724  usgrgt2cycl  35331  cusgracyclt3v  35357  sumeq2si  36403  prodeq2si  36405  cbvprodvw2  36448  cos2h  37949  tan2h  37950  lhpocnel2  40482  cdlemk19w  41435  lcmineqlem  42508  rencldnfilem  43269  imsqrtvalex  44094  frege70  44381  frege118  44429  hashnzfzclim  44770  dvradcnv2  44795  binomcxplemnotnn0  44804  supxrleubrnmptf  45900  ioonct  45988  fourierdlem112  46667  salexct2  46788  addmodne  47813  m1modnep2mod  47821  difmodm1lt  47828  2timesltsq  47841  2timesltsqm1  47842  flsqrt5  48072  lighneallem4b  48087  fpprel2  48232  gbegt5  48252  gbowgt5  48253  gbowge7  48254  gbege6  48256  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbalt  48272  sbgoldbm  48275  nnsum3primesle9  48285  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  tgblthelfgott  48306  gpg3kgrtriexlem5  48578