Theorem breq1i 5079

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

Syntax hints:   ↔ wb 207   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  eqbrtri  5093  brtpos0  8173  brtpos  8175  euen1  8964  euen1b  8965  2dom  8967  0sdom1domALT  9147  1sdom2  9148  modom2  9152  infglb  9394  infglbb  9395  cnfcom3lem  9615  axdclem2  10433  rnct  10438  cfpwsdom  10498  inar1  10689  reclem3pr  10963  gt0srpr  10992  mappsrpr  11022  ltpsrpr  11023  map2psrpr  11024  axpre-mulgt0  11082  lt0neg1  11647  le0neg1  11649  reclt1  12042  addltmul  12404  eluz2b1  12860  xlt0neg1  13162  xle0neg1  13164  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  elfznelfzo  13719  bernneq  14182  nn0opthlem1  14221  faclbnd4lem1  14246  hashge0  14340  hashgt23el  14377  hashge2el2difr  14434  cbvsum  15648  divcnvshft  15811  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  iprodmul  15959  oddge22np1  16309  nn0o1gt2  16341  divalglem1  16354  divalglem6  16358  isprm3  16643  dvdsnprmd  16650  2mulprm  16653  ge2nprmge4  16662  prmgaplem3  17015  isnzr2  20490  chrdvds  21501  chrcong  21502  lindsmm  21803  cpmidpmat  22856  csdfil  23877  iscau3  25263  ioombl1lem4  25546  itg2cn  25748  radcnvlt1  26401  sincosq1sgn  26480  sincosq3sgn  26482  sincosq4sgn  26483  ang180lem3  26793  leibpilem2  26923  issqf  27117  bposlem6  27270  gausslemma2dlem3  27349  nosupinfsep  27714  addcuts  27988  mulcut  28142  mulscan2d  28189  recsex  28229  absnegs  28257  avglts1d  28463  avglts2d  28464  z12bdaylem1  28480  z12bday  28495  bdayfin  28497  clwlkclwwlklem2  30088  clwlkclwwlk2  30091  clwlkclwwlkf  30096  clwlknf1oclwwlknlem1  30169  konigsberglem5  30344  cvexchi  32458  addltmulALT  32535  xnn01gt  32862  dya2iocct  34464  ballotlemi1  34687  signswch  34745  usgrgt2cycl  35358  cusgracyclt3v  35384  sumeq2si  36430  prodeq2si  36432  cbvprodvw2  36475  cos2h  37978  tan2h  37979  lhpocnel2  40511  cdlemk19w  41464  lcmineqlem  42537  rencldnfilem  43265  imsqrtvalex  44090  frege70  44377  frege118  44425  hashnzfzclim  44766  dvradcnv2  44791  binomcxplemnotnn0  44800  supxrleubrnmptf  45894  ioonct  45982  fourierdlem112  46661  salexct2  46782  addmodne  47813  m1modnep2mod  47821  difmodm1lt  47828  2timesltsq  47841  2timesltsqm1  47842  flsqrt5  48072  lighneallem4b  48087  fpprel2  48232  gbegt5  48252  gbowgt5  48253  gbowge7  48254  gbege6  48256  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbalt  48272  sbgoldbm  48275  nnsum3primesle9  48285  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  tgblthelfgott  48306  gpg3kgrtriexlem5  48578