Theorem breq1i 5110

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  eqbrtri  5126  brtpos0  8232  brtpos  8234  euen1  9036  euen1b  9037  2dom  9040  0sdom1domALT  9220  1sdom2  9221  modom2  9225  infglb  9464  infglbb  9465  cnfcom3lem  9685  axdclem2  10525  rnct  10531  cfpwsdom  10596  inar1  10787  reclem3pr  11061  gt0srpr  11090  mappsrpr  11120  ltpsrpr  11121  map2psrpr  11122  axpre-mulgt0  11180  lt0neg1  11747  le0neg1  11749  reclt1  12137  addltmul  12507  eluz2b1  12971  xlt0neg1  13274  xle0neg1  13276  iccshftr  13542  iccshftl  13544  iccdil  13546  icccntr  13548  elfznelfzo  13832  bernneq  14296  nn0opthlem1  14335  faclbnd4lem1  14360  hashge0  14454  hashgt23el  14492  hashge2el2difr  14549  cbvsum  15785  divcnvshft  15947  cbvprod  16005  cbvprodv  16006  prodeq1i  16008  iprodmul  16093  oddge22np1  16442  nn0o1gt2  16474  divalglem1  16487  divalglem6  16491  isprm3  16776  dvdsnprmd  16783  2mulprm  16786  ge2nprmge4  16795  prmgaplem3  17148  isnzr2  20681  chrdvds  21742  chrcong  21743  lindsmm  22044  cpmidpmat  23101  csdfil  24123  iscau3  25509  ioombl1lem4  25792  itg2cn  25994  radcnvlt1  26657  sincosq1sgn  26739  sincosq3sgn  26741  sincosq4sgn  26742  ang180lem3  27051  leibpilem2  27181  issqf  27375  bposlem6  27528  gausslemma2dlem3  27607  nosupinfsep  27971  addcuts  28246  mulcut  28400  mulscan2d  28447  recsex  28487  absnegs  28515  avglts1d  28721  avglts2d  28722  z12bdaylem1  28738  z12bday  28753  bdayfin  28755  clwlkclwwlklem2  30473  clwlkclwwlk2  30476  clwlkclwwlkf  30481  clwlknf1oclwwlknlem1  30554  konigsberglem5  30739  cvexchi  32853  addltmulALT  32930  xnn01gt  33244  dya2iocct  34794  ballotlemi1  35017  signswch  35072  usgrgt2cycl  35726  cusgracyclt3v  35738  sumeq2si  36825  prodeq2si  36827  cbvprodvw2  36870  cos2h  38368  tan2h  38369  lhpocnel2  40895  cdlemk19w  41848  lcmineqlem  42921  rencldnfilem  43664  imsqrtvalex  44489  frege70  44776  frege118  44824  hashnzfzclim  45149  dvradcnv2  45174  binomcxplemnotnn0  45183  supxrleubrnmptf  46282  ioonct  46370  fourierdlem112  47049  salexct2  47170  addmodne  48241  m1modnep2mod  48249  difmodm1lt  48256  2timesltsq  48269  2timesltsqm1  48270  flsqrt5  48500  lighneallem4b  48515  fpprel2  48660  gbegt5  48680  gbowgt5  48681  gbowge7  48682  gbege6  48684  sbgoldbwt  48696  sbgoldbst  48697  sbgoldbalt  48700  sbgoldbm  48703  nnsum3primesle9  48713  nnsum4primesevenALTV  48720  bgoldbtbndlem1  48724  tgblthelfgott  48734  gpg3kgrtriexlem5  49006