Theorem breq1i 5113

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  eqbrtri  5129  brtpos0  8264  brtpos  8266  euen1  9068  euen1b  9069  2dom  9072  0sdom1domALT  9252  1sdom2  9253  modom2  9257  infglb  9496  infglbb  9497  cnfcom3lem  9717  axdclem2  10611  rnct  10617  cfpwsdom  10682  inar1  10873  reclem3pr  11147  gt0srpr  11176  mappsrpr  11206  ltpsrpr  11207  map2psrpr  11208  axpre-mulgt0  11266  lt0neg1  11835  le0neg1  11837  reclt1  12225  addltmul  12595  eluz2b1  13059  xlt0neg1  13362  xle0neg1  13364  iccshftr  13630  iccshftl  13632  iccdil  13634  icccntr  13636  elfznelfzo  13921  bernneq  14386  nn0opthlem1  14425  faclbnd4lem1  14450  hashge0  14544  hashgt23el  14582  hashge2el2difr  14639  cbvsum  15877  divcnvshft  16039  cbvprod  16097  cbvprodv  16098  prodeq1i  16100  iprodmul  16185  oddge22np1  16534  nn0o1gt2  16566  divalglem1  16579  divalglem6  16583  isprm3  16873  dvdsnprmd  16880  2mulprm  16883  ge2nprmge4  16892  prmgaplem3  17246  isnzr2  20783  chrdvds  21847  chrcong  21848  lindsmm  22149  cpmidpmat  23206  csdfil  24228  iscau3  25614  ioombl1lem4  25897  itg2cn  26099  radcnvlt1  26760  sincosq1sgn  26842  sincosq3sgn  26844  sincosq4sgn  26845  ang180lem3  27154  leibpilem2  27284  issqf  27478  bposlem6  27631  gausslemma2dlem3  27710  fltoprmlem2  28009  fltoprmgt3  28011  nosupinfsep  28104  addcuts  28379  mulcut  28533  mulscan2d  28580  recsex  28620  absnegs  28648  avglts1d  28854  avglts2d  28855  z12bdaylem1  28871  z12bday  28886  bdayfin  28888  clwlkclwwlklem2  30606  clwlkclwwlk2  30609  clwlkclwwlkf  30614  clwlknf1oclwwlknlem1  30687  konigsberglem5  30872  cvexchi  32986  addltmulALT  33105  xnn01gt  33418  dya2iocct  34968  ballotlemi1  35191  signswch  35246  usgrgt2cycl  36023  cusgracyclt3v  36035  sumeq2si  37121  prodeq2si  37123  cbvprodvw2  37166  cos2h  38677  tan2h  38678  lhpocnel2  41219  cdlemk19w  42172  lcmineqlem  43245  rencldnfilem  43970  imsqrtvalex  44789  frege70  45076  frege118  45124  hashnzfzclim  45449  dvradcnv2  45474  binomcxplemnotnn0  45483  supxrleubrnmptf  46603  ioonct  46691  fourierdlem112  47370  salexct2  47491  addmodne  48562  m1modnep2mod  48570  difmodm1lt  48577  2timesltsq  48590  2timesltsqm1  48591  flsqrt5  48821  lighneallem4b  48836  fpprel2  48981  gbegt5  49001  gbowgt5  49002  gbowge7  49003  gbege6  49005  sbgoldbwt  49017  sbgoldbst  49018  sbgoldbalt  49021  sbgoldbm  49024  nnsum3primesle9  49034  nnsum4primesevenALTV  49041  bgoldbtbndlem1  49045  tgblthelfgott  49055  gpg3kgrtriexlem5  49327