Theorem breq1i 5173

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

Syntax hints:   ↔ wb 206   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  eqbrtri  5187  brtpos0  8274  brtpos  8276  euen1  9091  euen1b  9092  2dom  9095  0sdom1domALT  9302  1sdom2  9303  modom2  9308  1sdomOLD  9312  infglb  9559  infglbb  9560  cnfcom3lem  9772  pr2nelemOLD  10072  axdclem2  10589  rnct  10594  cfpwsdom  10653  inar1  10844  reclem3pr  11118  gt0srpr  11147  mappsrpr  11177  ltpsrpr  11178  map2psrpr  11179  axpre-mulgt0  11237  lt0neg1  11796  le0neg1  11798  reclt1  12190  addltmul  12529  eluz2b1  12984  xlt0neg1  13281  xle0neg1  13283  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  elfznelfzo  13822  bernneq  14278  nn0opthlem1  14317  faclbnd4lem1  14342  hashge0  14436  hashgt23el  14473  hashge2el2difr  14530  cbvsum  15743  divcnvshft  15903  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  iprodmul  16051  oddge22np1  16397  nn0o1gt2  16429  divalglem1  16442  divalglem6  16446  isprm3  16730  dvdsnprmd  16737  2mulprm  16740  ge2nprmge4  16748  prmgaplem3  17100  isnzr2  20544  chrdvds  21564  chrcong  21565  lindsmm  21871  cpmidpmat  22900  csdfil  23923  iscau3  25331  ioombl1lem4  25615  itg2cn  25818  radcnvlt1  26479  sincosq1sgn  26558  sincosq3sgn  26560  sincosq4sgn  26561  ang180lem3  26872  leibpilem2  27002  issqf  27197  bposlem6  27351  gausslemma2dlem3  27430  nosupinfsep  27795  addscut  28029  mulscut  28176  mulscan2d  28223  recsex  28261  abssneg  28289  clwlkclwwlklem2  30032  clwlkclwwlk2  30035  clwlkclwwlkf  30040  clwlknf1oclwwlknlem1  30113  konigsberglem5  30288  cvexchi  32401  addltmulALT  32478  xnn01gt  32777  dya2iocct  34245  ballotlemi1  34467  signswch  34538  usgrgt2cycl  35098  cusgracyclt3v  35124  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36213  cos2h  37571  tan2h  37572  lhpocnel2  39976  cdlemk19w  40929  lcmineqlem  42009  rencldnfilem  42776  imsqrtvalex  43608  frege70  43895  frege118  43943  hashnzfzclim  44291  dvradcnv2  44316  binomcxplemnotnn0  44325  supxrleubrnmptf  45366  ioonct  45455  fourierdlem112  46139  salexct2  46260  flsqrt5  47468  lighneallem4b  47483  fpprel2  47615  gbegt5  47635  gbowgt5  47636  gbowge7  47637  gbege6  47639  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbalt  47655  sbgoldbm  47658  nnsum3primesle9  47668  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  tgblthelfgott  47689  difmodm1lt  48256