Theorem breq1i 5096

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

Syntax hints:   ↔ wb 206   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  eqbrtri  5110  brtpos0  8163  brtpos  8165  euen1  8949  euen1b  8950  2dom  8952  0sdom1domALT  9131  1sdom2  9132  modom2  9136  infglb  9375  infglbb  9376  cnfcom3lem  9593  axdclem2  10411  rnct  10416  cfpwsdom  10475  inar1  10666  reclem3pr  10940  gt0srpr  10969  mappsrpr  10999  ltpsrpr  11000  map2psrpr  11001  axpre-mulgt0  11059  lt0neg1  11623  le0neg1  11625  reclt1  12017  addltmul  12357  eluz2b1  12817  xlt0neg1  13118  xle0neg1  13120  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  elfznelfzo  13673  bernneq  14136  nn0opthlem1  14175  faclbnd4lem1  14200  hashge0  14294  hashgt23el  14331  hashge2el2difr  14388  cbvsum  15602  divcnvshft  15762  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  iprodmul  15910  oddge22np1  16260  nn0o1gt2  16292  divalglem1  16305  divalglem6  16309  isprm3  16594  dvdsnprmd  16601  2mulprm  16604  ge2nprmge4  16612  prmgaplem3  16965  isnzr2  20433  chrdvds  21463  chrcong  21464  lindsmm  21765  cpmidpmat  22788  csdfil  23809  iscau3  25205  ioombl1lem4  25489  itg2cn  25691  radcnvlt1  26354  sincosq1sgn  26434  sincosq3sgn  26436  sincosq4sgn  26437  ang180lem3  26748  leibpilem2  26878  issqf  27073  bposlem6  27227  gausslemma2dlem3  27306  nosupinfsep  27671  addscut  27921  mulscut  28071  mulscan2d  28118  recsex  28157  abssneg  28185  avgslt1d  28376  avgslt2d  28377  clwlkclwwlklem2  29980  clwlkclwwlk2  29983  clwlkclwwlkf  29988  clwlknf1oclwwlknlem1  30061  konigsberglem5  30236  cvexchi  32349  addltmulALT  32426  xnn01gt  32753  dya2iocct  34293  ballotlemi1  34516  signswch  34574  usgrgt2cycl  35174  cusgracyclt3v  35200  sumeq2si  36246  prodeq2si  36248  cbvprodvw2  36291  cos2h  37661  tan2h  37662  lhpocnel2  40128  cdlemk19w  41081  lcmineqlem  42155  rencldnfilem  42923  imsqrtvalex  43749  frege70  44036  frege118  44084  hashnzfzclim  44425  dvradcnv2  44450  binomcxplemnotnn0  44459  supxrleubrnmptf  45559  ioonct  45647  fourierdlem112  46326  salexct2  46447  addmodne  47454  m1modnep2mod  47462  difmodm1lt  47469  flsqrt5  47704  lighneallem4b  47719  fpprel2  47851  gbegt5  47871  gbowgt5  47872  gbowge7  47873  gbege6  47875  sbgoldbwt  47887  sbgoldbst  47888  sbgoldbalt  47891  sbgoldbm  47894  nnsum3primesle9  47904  nnsum4primesevenALTV  47911  bgoldbtbndlem1  47915  tgblthelfgott  47925  gpg3kgrtriexlem5  48197