Theorem breq1i 5107

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  eqbrtri  5121  brtpos0  8185  brtpos  8187  euen1  8976  euen1b  8977  2dom  8979  0sdom1domALT  9159  1sdom2  9160  modom2  9164  infglb  9406  infglbb  9407  cnfcom3lem  9624  axdclem2  10442  rnct  10447  cfpwsdom  10507  inar1  10698  reclem3pr  10972  gt0srpr  11001  mappsrpr  11031  ltpsrpr  11032  map2psrpr  11033  axpre-mulgt0  11091  lt0neg1  11655  le0neg1  11657  reclt1  12049  addltmul  12389  eluz2b1  12844  xlt0neg1  13146  xle0neg1  13148  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  elfznelfzo  13701  bernneq  14164  nn0opthlem1  14203  faclbnd4lem1  14228  hashge0  14322  hashgt23el  14359  hashge2el2difr  14416  cbvsum  15630  divcnvshft  15790  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  iprodmul  15938  oddge22np1  16288  nn0o1gt2  16320  divalglem1  16333  divalglem6  16337  isprm3  16622  dvdsnprmd  16629  2mulprm  16632  ge2nprmge4  16640  prmgaplem3  16993  isnzr2  20466  chrdvds  21496  chrcong  21497  lindsmm  21798  cpmidpmat  22832  csdfil  23853  iscau3  25249  ioombl1lem4  25533  itg2cn  25735  radcnvlt1  26398  sincosq1sgn  26478  sincosq3sgn  26480  sincosq4sgn  26481  ang180lem3  26792  leibpilem2  26922  issqf  27117  bposlem6  27271  gausslemma2dlem3  27350  nosupinfsep  27715  addcuts  27989  mulcut  28143  mulscan2d  28190  recsex  28230  absnegs  28258  avglts1d  28464  avglts2d  28465  z12bdaylem1  28481  z12bday  28496  bdayfin  28498  clwlkclwwlklem2  30091  clwlkclwwlk2  30094  clwlkclwwlkf  30099  clwlknf1oclwwlknlem1  30172  konigsberglem5  30347  cvexchi  32461  addltmulALT  32538  xnn01gt  32865  dya2iocct  34462  ballotlemi1  34685  signswch  34743  usgrgt2cycl  35350  cusgracyclt3v  35376  sumeq2si  36422  prodeq2si  36424  cbvprodvw2  36467  cos2h  37866  tan2h  37867  lhpocnel2  40399  cdlemk19w  41352  lcmineqlem  42426  rencldnfilem  43181  imsqrtvalex  44006  frege70  44293  frege118  44341  hashnzfzclim  44682  dvradcnv2  44707  binomcxplemnotnn0  44716  supxrleubrnmptf  45813  ioonct  45901  fourierdlem112  46580  salexct2  46701  addmodne  47708  m1modnep2mod  47716  difmodm1lt  47723  flsqrt5  47958  lighneallem4b  47973  fpprel2  48105  gbegt5  48125  gbowgt5  48126  gbowge7  48127  gbege6  48129  sbgoldbwt  48141  sbgoldbst  48142  sbgoldbalt  48145  sbgoldbm  48148  nnsum3primesle9  48158  nnsum4primesevenALTV  48165  bgoldbtbndlem1  48169  tgblthelfgott  48179  gpg3kgrtriexlem5  48451