Theorem breq1i 5092

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  eqbrtri  5106  brtpos0  8183  brtpos  8185  euen1  8974  euen1b  8975  2dom  8977  0sdom1domALT  9157  1sdom2  9158  modom2  9162  infglb  9404  infglbb  9405  cnfcom3lem  9624  axdclem2  10442  rnct  10447  cfpwsdom  10507  inar1  10698  reclem3pr  10972  gt0srpr  11001  mappsrpr  11031  ltpsrpr  11032  map2psrpr  11033  axpre-mulgt0  11091  lt0neg1  11656  le0neg1  11658  reclt1  12051  addltmul  12413  eluz2b1  12869  xlt0neg1  13171  xle0neg1  13173  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  elfznelfzo  13728  bernneq  14191  nn0opthlem1  14230  faclbnd4lem1  14255  hashge0  14349  hashgt23el  14386  hashge2el2difr  14443  cbvsum  15657  divcnvshft  15820  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  iprodmul  15968  oddge22np1  16318  nn0o1gt2  16350  divalglem1  16363  divalglem6  16367  isprm3  16652  dvdsnprmd  16659  2mulprm  16662  ge2nprmge4  16671  prmgaplem3  17024  isnzr2  20495  chrdvds  21506  chrcong  21507  lindsmm  21808  cpmidpmat  22838  csdfil  23859  iscau3  25245  ioombl1lem4  25528  itg2cn  25730  radcnvlt1  26383  sincosq1sgn  26462  sincosq3sgn  26464  sincosq4sgn  26465  ang180lem3  26775  leibpilem2  26905  issqf  27099  bposlem6  27252  gausslemma2dlem3  27331  nosupinfsep  27696  addcuts  27970  mulcut  28124  mulscan2d  28171  recsex  28211  absnegs  28239  avglts1d  28445  avglts2d  28446  z12bdaylem1  28462  z12bday  28477  bdayfin  28479  clwlkclwwlklem2  30070  clwlkclwwlk2  30073  clwlkclwwlkf  30078  clwlknf1oclwwlknlem1  30151  konigsberglem5  30326  cvexchi  32440  addltmulALT  32517  xnn01gt  32843  dya2iocct  34424  ballotlemi1  34647  signswch  34705  usgrgt2cycl  35312  cusgracyclt3v  35338  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  cos2h  37932  tan2h  37933  lhpocnel2  40465  cdlemk19w  41418  lcmineqlem  42491  rencldnfilem  43248  imsqrtvalex  44073  frege70  44360  frege118  44408  hashnzfzclim  44749  dvradcnv2  44774  binomcxplemnotnn0  44783  supxrleubrnmptf  45879  ioonct  45967  fourierdlem112  46646  salexct2  46767  addmodne  47798  m1modnep2mod  47806  difmodm1lt  47813  2timesltsq  47826  2timesltsqm1  47827  flsqrt5  48057  lighneallem4b  48072  fpprel2  48217  gbegt5  48237  gbowgt5  48238  gbowge7  48239  gbege6  48241  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbalt  48257  sbgoldbm  48260  nnsum3primesle9  48270  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  tgblthelfgott  48291  gpg3kgrtriexlem5  48563