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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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  8250  brtpos  8252  euen1  9054  euen1b  9055  2dom  9058  0sdom1domALT  9238  1sdom2  9239  modom2  9243  infglb  9483  infglbb  9484  cnfcom3lem  9704  axdclem2  10598  rnct  10604  cfpwsdom  10669  inar1  10860  reclem3pr  11134  gt0srpr  11163  mappsrpr  11193  ltpsrpr  11194  map2psrpr  11195  axpre-mulgt0  11253  lt0neg1  11822  le0neg1  11824  reclt1  12212  addltmul  12582  eluz2b1  13046  xlt0neg1  13349  xle0neg1  13351  iccshftr  13617  iccshftl  13619  iccdil  13621  icccntr  13623  elfznelfzo  13908  bernneq  14373  nn0opthlem1  14412  faclbnd4lem1  14437  hashge0  14531  hashgt23el  14569  hashge2el2difr  14626  cbvsum  15862  divcnvshft  16024  cbvprod  16082  cbvprodv  16083  prodeq1i  16085  iprodmul  16170  oddge22np1  16519  nn0o1gt2  16551  divalglem1  16564  divalglem6  16568  isprm3  16858  dvdsnprmd  16865  2mulprm  16868  ge2nprmge4  16877  prmgaplem3  17231  isnzr2  20768  chrdvds  21832  chrcong  21833  lindsmm  22134  cpmidpmat  23191  csdfil  24213  iscau3  25599  ioombl1lem4  25882  itg2cn  26084  radcnvlt1  26745  sincosq1sgn  26827  sincosq3sgn  26829  sincosq4sgn  26830  ang180lem3  27139  leibpilem2  27269  issqf  27463  bposlem6  27616  gausslemma2dlem3  27695  fltoprmlem2  27994  fltoprmgt3  27996  nosupinfsep  28089  addcuts  28364  mulcut  28518  mulscan2d  28565  recsex  28605  absnegs  28633  avglts1d  28839  avglts2d  28840  z12bdaylem1  28856  z12bday  28871  bdayfin  28873  clwlkclwwlklem2  30591  clwlkclwwlk2  30594  clwlkclwwlkf  30599  clwlknf1oclwwlknlem1  30672  konigsberglem5  30857  cvexchi  32971  addltmulALT  33048  xnn01gt  33362  dya2iocct  34912  ballotlemi1  35135  signswch  35190  usgrgt2cycl  35909  cusgracyclt3v  35921  sumeq2si  36991  prodeq2si  36993  cbvprodvw2  37036  cos2h  38534  tan2h  38535  lhpocnel2  41076  cdlemk19w  42029  lcmineqlem  43102  rencldnfilem  43826  imsqrtvalex  44645  frege70  44932  frege118  44980  hashnzfzclim  45305  dvradcnv2  45330  binomcxplemnotnn0  45339  supxrleubrnmptf  46460  ioonct  46548  fourierdlem112  47227  salexct2  47348  addmodne  48419  m1modnep2mod  48427  difmodm1lt  48434  2timesltsq  48447  2timesltsqm1  48448  flsqrt5  48678  lighneallem4b  48693  fpprel2  48838  gbegt5  48858  gbowgt5  48859  gbowge7  48860  gbege6  48862  sbgoldbwt  48874  sbgoldbst  48875  sbgoldbalt  48878  sbgoldbm  48881  nnsum3primesle9  48891  nnsum4primesevenALTV  48898  bgoldbtbndlem1  48902  tgblthelfgott  48912  gpg3kgrtriexlem5  49184