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  27462  mulscut  27588  mulscan2d  27631  recsex  27665  clwlkclwwlklem2  29253  clwlkclwwlk2  29256  clwlkclwwlkf  29261  clwlknf1oclwwlknlem1  29334  konigsberglem5  29509  cvexchi  31622  addltmulALT  31699  xnn01gt  31983  dya2iocct  33279  ballotlemi1  33501  signswch  33572  usgrgt2cycl  34121  cusgracyclt3v  34147  cos2h  36479  tan2h  36480  lhpocnel2  38890  cdlemk19w  39843  lcmineqlem  40917  rencldnfilem  41558  imsqrtvalex  42397  frege70  42684  frege118  42732  hashnzfzclim  43081  dvradcnv2  43106  binomcxplemnotnn0  43115  supxrleubrnmptf  44161  ioonct  44250  fourierdlem112  44934  salexct2  45055  flsqrt5  46262  lighneallem4b  46277  fpprel2  46409  gbegt5  46429  gbowgt5  46430  gbowge7  46431  gbege6  46433  sbgoldbwt  46445  sbgoldbst  46446  sbgoldbalt  46449  sbgoldbm  46452  nnsum3primesle9  46462  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  tgblthelfgott  46483  difmodm1lt  47208