Theorem breq1i 5156

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

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

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  eqbrtri  5170  brtpos0  8218  brtpos  8220  euen1  9026  euen1b  9027  2dom  9030  0sdom1domALT  9239  1sdom2  9240  modom2  9245  1sdomOLD  9249  infglb  9485  infglbb  9486  cnfcom3lem  9698  pr2nelemOLD  9998  axdclem2  10515  rnct  10520  cfpwsdom  10579  inar1  10770  reclem3pr  11044  gt0srpr  11073  mappsrpr  11103  ltpsrpr  11104  map2psrpr  11105  axpre-mulgt0  11163  lt0neg1  11720  le0neg1  11722  reclt1  12109  addltmul  12448  eluz2b1  12903  xlt0neg1  13198  xle0neg1  13200  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  elfznelfzo  13737  bernneq  14192  nn0opthlem1  14228  faclbnd4lem1  14253  hashge0  14347  hashgt23el  14384  hashge2el2difr  14442  cbvsum  15641  divcnvshft  15801  cbvprod  15859  iprodmul  15947  oddge22np1  16292  nn0o1gt2  16324  divalglem1  16337  divalglem6  16341  isprm3  16620  dvdsnprmd  16627  2mulprm  16630  ge2nprmge4  16638  prmgaplem3  16986  isnzr2  20297  chrdvds  21080  chrcong  21081  lindsmm  21383  cpmidpmat  22375  csdfil  23398  iscau3  24795  ioombl1lem4  25078  itg2cn  25281  radcnvlt1  25930  sincosq1sgn  26008  sincosq3sgn  26010  sincosq4sgn  26011  ang180lem3  26316  leibpilem2  26446  issqf  26640  bposlem6  26792  gausslemma2dlem3  26871  nosupinfsep  27235  addscut  27464  mulscut  27591  mulscan2d  27634  recsex  27668  clwlkclwwlklem2  29284  clwlkclwwlk2  29287  clwlkclwwlkf  29292  clwlknf1oclwwlknlem1  29365  konigsberglem5  29540  cvexchi  31653  addltmulALT  31730  xnn01gt  32014  dya2iocct  33310  ballotlemi1  33532  signswch  33603  usgrgt2cycl  34152  cusgracyclt3v  34178  cos2h  36527  tan2h  36528  lhpocnel2  38938  cdlemk19w  39891  lcmineqlem  40965  rencldnfilem  41606  imsqrtvalex  42445  frege70  42732  frege118  42780  hashnzfzclim  43129  dvradcnv2  43154  binomcxplemnotnn0  43163  supxrleubrnmptf  44209  ioonct  44298  fourierdlem112  44982  salexct2  45103  flsqrt5  46310  lighneallem4b  46325  fpprel2  46457  gbegt5  46477  gbowgt5  46478  gbowge7  46479  gbege6  46481  sbgoldbwt  46493  sbgoldbst  46494  sbgoldbalt  46497  sbgoldbm  46500  nnsum3primesle9  46510  nnsum4primesevenALTV  46517  bgoldbtbndlem1  46521  tgblthelfgott  46531  difmodm1lt  47256