Theorem breq1i 5120

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

Syntax hints:   ↔ wb 209   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  eqbrtri  5136  brtpos0  8229  brtpos  8231  euen1  9024  euen1b  9025  2dom  9027  0sdom1domALT  9207  1sdom2  9208  modom2  9212  infglb  9451  infglbb  9452  cnfcom3lem  9672  axdclem2  10504  rnct  10509  cfpwsdom  10569  inar1  10760  reclem3pr  11034  gt0srpr  11063  mappsrpr  11093  ltpsrpr  11094  map2psrpr  11095  axpre-mulgt0  11153  lt0neg1  11720  le0neg1  11722  reclt1  12110  addltmul  12480  eluz2b1  12943  xlt0neg1  13245  xle0neg1  13247  iccshftr  13513  iccshftl  13515  iccdil  13517  icccntr  13519  elfznelfzo  13802  bernneq  14265  nn0opthlem1  14304  faclbnd4lem1  14329  hashge0  14423  hashgt23el  14461  hashge2el2difr  14518  cbvsum  15746  divcnvshft  15909  cbvprod  15967  cbvprodv  15968  prodeq1i  15970  iprodmul  16057  oddge22np1  16407  nn0o1gt2  16439  divalglem1  16452  divalglem6  16456  isprm3  16741  dvdsnprmd  16748  2mulprm  16751  ge2nprmge4  16760  prmgaplem3  17113  isnzr2  20601  chrdvds  21645  chrcong  21646  lindsmm  21947  cpmidpmat  22999  csdfil  24020  iscau3  25406  ioombl1lem4  25689  itg2cn  25891  radcnvlt1  26547  sincosq1sgn  26629  sincosq3sgn  26631  sincosq4sgn  26632  ang180lem3  26942  leibpilem2  27072  issqf  27266  bposlem6  27419  gausslemma2dlem3  27498  nosupinfsep  27862  addcuts  28137  mulcut  28291  mulscan2d  28338  recsex  28378  absnegs  28406  avglts1d  28612  avglts2d  28613  z12bdaylem1  28629  z12bday  28644  bdayfin  28646  clwlkclwwlklem2  30292  clwlkclwwlk2  30295  clwlkclwwlkf  30300  clwlknf1oclwwlknlem1  30373  konigsberglem5  30548  cvexchi  32662  addltmulALT  32739  xnn01gt  33056  dya2iocct  34615  ballotlemi1  34838  signswch  34893  usgrgt2cycl  35555  cusgracyclt3v  35581  sumeq2si  36637  prodeq2si  36639  cbvprodvw2  36682  cos2h  38184  tan2h  38185  lhpocnel2  40717  cdlemk19w  41670  lcmineqlem  42743  rencldnfilem  43473  imsqrtvalex  44298  frege70  44585  frege118  44633  hashnzfzclim  44958  dvradcnv2  44983  binomcxplemnotnn0  44992  supxrleubrnmptf  46091  ioonct  46179  fourierdlem112  46858  salexct2  46979  addmodne  48010  m1modnep2mod  48018  difmodm1lt  48025  2timesltsq  48038  2timesltsqm1  48039  flsqrt5  48269  lighneallem4b  48284  fpprel2  48429  gbegt5  48449  gbowgt5  48450  gbowge7  48451  gbege6  48453  sbgoldbwt  48465  sbgoldbst  48466  sbgoldbalt  48469  sbgoldbm  48472  nnsum3primesle9  48482  nnsum4primesevenALTV  48489  bgoldbtbndlem1  48493  tgblthelfgott  48503  gpg3kgrtriexlem5  48775