Theorem breq1i 5118

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  eqbrtri  5134  brtpos0  8235  brtpos  8237  euen1  9030  euen1b  9031  2dom  9034  0sdom1domALT  9214  1sdom2  9215  modom2  9219  infglb  9458  infglbb  9459  cnfcom3lem  9679  axdclem2  10519  rnct  10525  cfpwsdom  10588  inar1  10779  reclem3pr  11053  gt0srpr  11082  mappsrpr  11112  ltpsrpr  11113  map2psrpr  11114  axpre-mulgt0  11172  lt0neg1  11739  le0neg1  11741  reclt1  12129  addltmul  12499  eluz2b1  12963  xlt0neg1  13265  xle0neg1  13267  iccshftr  13533  iccshftl  13535  iccdil  13537  icccntr  13539  elfznelfzo  13823  bernneq  14287  nn0opthlem1  14326  faclbnd4lem1  14351  hashge0  14445  hashgt23el  14483  hashge2el2difr  14540  cbvsum  15774  divcnvshft  15936  cbvprod  15994  cbvprodv  15995  prodeq1i  15997  iprodmul  16084  oddge22np1  16433  nn0o1gt2  16465  divalglem1  16478  divalglem6  16482  isprm3  16767  dvdsnprmd  16774  2mulprm  16777  ge2nprmge4  16786  prmgaplem3  17139  isnzr2  20669  chrdvds  21730  chrcong  21731  lindsmm  22032  cpmidpmat  23084  csdfil  24106  iscau3  25492  ioombl1lem4  25775  itg2cn  25977  radcnvlt1  26636  sincosq1sgn  26718  sincosq3sgn  26720  sincosq4sgn  26721  ang180lem3  27031  leibpilem2  27161  issqf  27355  bposlem6  27508  gausslemma2dlem3  27587  nosupinfsep  27951  addcuts  28226  mulcut  28380  mulscan2d  28427  recsex  28467  absnegs  28495  avglts1d  28701  avglts2d  28702  z12bdaylem1  28718  z12bday  28733  bdayfin  28735  clwlkclwwlklem2  30422  clwlkclwwlk2  30425  clwlkclwwlkf  30430  clwlknf1oclwwlknlem1  30503  konigsberglem5  30682  cvexchi  32796  addltmulALT  32873  xnn01gt  33189  dya2iocct  34739  ballotlemi1  34962  signswch  35017  usgrgt2cycl  35671  cusgracyclt3v  35689  sumeq2si  36775  prodeq2si  36777  cbvprodvw2  36820  cos2h  38323  tan2h  38324  lhpocnel2  40855  cdlemk19w  41808  lcmineqlem  42881  rencldnfilem  43624  imsqrtvalex  44449  frege70  44736  frege118  44784  hashnzfzclim  45109  dvradcnv2  45134  binomcxplemnotnn0  45143  supxrleubrnmptf  46242  ioonct  46330  fourierdlem112  47009  salexct2  47130  addmodne  48164  m1modnep2mod  48172  difmodm1lt  48179  2timesltsq  48192  2timesltsqm1  48193  flsqrt5  48423  lighneallem4b  48438  fpprel2  48583  gbegt5  48603  gbowgt5  48604  gbowge7  48605  gbege6  48607  sbgoldbwt  48619  sbgoldbst  48620  sbgoldbalt  48623  sbgoldbm  48626  nnsum3primesle9  48636  nnsum4primesevenALTV  48643  bgoldbtbndlem1  48647  tgblthelfgott  48657  gpg3kgrtriexlem5  48929