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  38535  tan2h  38536  lhpocnel2  41077  cdlemk19w  42030  lcmineqlem  43103  rencldnfilem  43827  imsqrtvalex  44646  frege70  44933  frege118  44981  hashnzfzclim  45306  dvradcnv2  45331  binomcxplemnotnn0  45340  supxrleubrnmptf  46461  ioonct  46549  fourierdlem112  47228  salexct2  47349  addmodne  48420  m1modnep2mod  48428  difmodm1lt  48435  2timesltsq  48448  2timesltsqm1  48449  flsqrt5  48679  lighneallem4b  48694  fpprel2  48839  gbegt5  48859  gbowgt5  48860  gbowge7  48861  gbege6  48863  sbgoldbwt  48875  sbgoldbst  48876  sbgoldbalt  48879  sbgoldbm  48882  nnsum3primesle9  48892  nnsum4primesevenALTV  48899  bgoldbtbndlem1  48903  tgblthelfgott  48913  gpg3kgrtriexlem5  49185