Theorem breq1i 5109

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  eqbrtri  5123  brtpos0  8189  brtpos  8191  euen1  8975  euen1b  8976  2dom  8978  0sdom1domALT  9163  1sdom2  9164  modom2  9168  1sdomOLD  9172  infglb  9418  infglbb  9419  cnfcom3lem  9632  pr2nelemOLD  9932  axdclem2  10449  rnct  10454  cfpwsdom  10513  inar1  10704  reclem3pr  10978  gt0srpr  11007  mappsrpr  11037  ltpsrpr  11038  map2psrpr  11039  axpre-mulgt0  11097  lt0neg1  11660  le0neg1  11662  reclt1  12054  addltmul  12394  eluz2b1  12854  xlt0neg1  13155  xle0neg1  13157  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  elfznelfzo  13709  bernneq  14170  nn0opthlem1  14209  faclbnd4lem1  14234  hashge0  14328  hashgt23el  14365  hashge2el2difr  14422  cbvsum  15637  divcnvshft  15797  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  iprodmul  15945  oddge22np1  16295  nn0o1gt2  16327  divalglem1  16340  divalglem6  16344  isprm3  16629  dvdsnprmd  16636  2mulprm  16639  ge2nprmge4  16647  prmgaplem3  17000  isnzr2  20438  chrdvds  21468  chrcong  21469  lindsmm  21770  cpmidpmat  22793  csdfil  23814  iscau3  25211  ioombl1lem4  25495  itg2cn  25697  radcnvlt1  26360  sincosq1sgn  26440  sincosq3sgn  26442  sincosq4sgn  26443  ang180lem3  26754  leibpilem2  26884  issqf  27079  bposlem6  27233  gausslemma2dlem3  27312  nosupinfsep  27677  addscut  27925  mulscut  28075  mulscan2d  28122  recsex  28161  abssneg  28189  avgslt1d  28379  avgslt2d  28380  clwlkclwwlklem2  29979  clwlkclwwlk2  29982  clwlkclwwlkf  29987  clwlknf1oclwwlknlem1  30060  konigsberglem5  30235  cvexchi  32348  addltmulALT  32425  xnn01gt  32743  dya2iocct  34264  ballotlemi1  34487  signswch  34545  usgrgt2cycl  35110  cusgracyclt3v  35136  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36228  cos2h  37598  tan2h  37599  lhpocnel2  40006  cdlemk19w  40959  lcmineqlem  42033  rencldnfilem  42801  imsqrtvalex  43628  frege70  43915  frege118  43963  hashnzfzclim  44304  dvradcnv2  44329  binomcxplemnotnn0  44338  supxrleubrnmptf  45440  ioonct  45528  fourierdlem112  46209  salexct2  46330  addmodne  47338  m1modnep2mod  47346  difmodm1lt  47353  flsqrt5  47588  lighneallem4b  47603  fpprel2  47735  gbegt5  47755  gbowgt5  47756  gbowge7  47757  gbege6  47759  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbalt  47775  sbgoldbm  47778  nnsum3primesle9  47788  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  tgblthelfgott  47809  gpg3kgrtriexlem5  48071