Theorem breq1i 5093

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

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtri  5107  brtpos0  8176  brtpos  8178  euen1  8967  euen1b  8968  2dom  8970  0sdom1domALT  9150  1sdom2  9151  modom2  9155  infglb  9397  infglbb  9398  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  20486  chrdvds  21516  chrcong  21517  lindsmm  21818  cpmidpmat  22848  csdfil  23869  iscau3  25255  ioombl1lem4  25538  itg2cn  25740  radcnvlt1  26396  sincosq1sgn  26475  sincosq3sgn  26477  sincosq4sgn  26478  ang180lem3  26788  leibpilem2  26918  issqf  27113  bposlem6  27266  gausslemma2dlem3  27345  nosupinfsep  27710  addcuts  27984  mulcut  28138  mulscan2d  28185  recsex  28225  absnegs  28253  avglts1d  28459  avglts2d  28460  z12bdaylem1  28476  z12bday  28491  bdayfin  28493  clwlkclwwlklem2  30085  clwlkclwwlk2  30088  clwlkclwwlkf  30093  clwlknf1oclwwlknlem1  30166  konigsberglem5  30341  cvexchi  32455  addltmulALT  32532  xnn01gt  32858  dya2iocct  34440  ballotlemi1  34663  signswch  34721  usgrgt2cycl  35328  cusgracyclt3v  35354  sumeq2si  36400  prodeq2si  36402  cbvprodvw2  36445  cos2h  37946  tan2h  37947  lhpocnel2  40479  cdlemk19w  41432  lcmineqlem  42505  rencldnfilem  43266  imsqrtvalex  44091  frege70  44378  frege118  44426  hashnzfzclim  44767  dvradcnv2  44792  binomcxplemnotnn0  44801  supxrleubrnmptf  45897  ioonct  45985  fourierdlem112  46664  salexct2  46785  addmodne  47810  m1modnep2mod  47818  difmodm1lt  47825  2timesltsq  47838  2timesltsqm1  47839  flsqrt5  48069  lighneallem4b  48084  fpprel2  48229  gbegt5  48249  gbowgt5  48250  gbowge7  48251  gbege6  48253  sbgoldbwt  48265  sbgoldbst  48266  sbgoldbalt  48269  sbgoldbm  48272  nnsum3primesle9  48282  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  tgblthelfgott  48303  gpg3kgrtriexlem5  48575