Theorem breq1i 5103

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

Syntax hints:   ↔ wb 206   = wceq 1541   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  eqbrtri  5117  brtpos0  8173  brtpos  8175  euen1  8962  euen1b  8963  2dom  8965  0sdom1domALT  9145  1sdom2  9146  modom2  9150  infglb  9392  infglbb  9393  cnfcom3lem  9610  axdclem2  10428  rnct  10433  cfpwsdom  10493  inar1  10684  reclem3pr  10958  gt0srpr  10987  mappsrpr  11017  ltpsrpr  11018  map2psrpr  11019  axpre-mulgt0  11077  lt0neg1  11641  le0neg1  11643  reclt1  12035  addltmul  12375  eluz2b1  12830  xlt0neg1  13132  xle0neg1  13134  iccshftr  13400  iccshftl  13402  iccdil  13404  icccntr  13406  elfznelfzo  13687  bernneq  14150  nn0opthlem1  14189  faclbnd4lem1  14214  hashge0  14308  hashgt23el  14345  hashge2el2difr  14402  cbvsum  15616  divcnvshft  15776  cbvprod  15834  cbvprodv  15835  prodeq1i  15837  iprodmul  15924  oddge22np1  16274  nn0o1gt2  16306  divalglem1  16319  divalglem6  16323  isprm3  16608  dvdsnprmd  16615  2mulprm  16618  ge2nprmge4  16626  prmgaplem3  16979  isnzr2  20449  chrdvds  21479  chrcong  21480  lindsmm  21781  cpmidpmat  22815  csdfil  23836  iscau3  25232  ioombl1lem4  25516  itg2cn  25718  radcnvlt1  26381  sincosq1sgn  26461  sincosq3sgn  26463  sincosq4sgn  26464  ang180lem3  26775  leibpilem2  26905  issqf  27100  bposlem6  27254  gausslemma2dlem3  27333  nosupinfsep  27698  addscut  27948  mulscut  28101  mulscan2d  28148  recsex  28187  abssneg  28215  avgslt1d  28411  avgslt2d  28412  clwlkclwwlklem2  30024  clwlkclwwlk2  30027  clwlkclwwlkf  30032  clwlknf1oclwwlknlem1  30105  konigsberglem5  30280  cvexchi  32393  addltmulALT  32470  xnn01gt  32799  dya2iocct  34386  ballotlemi1  34609  signswch  34667  usgrgt2cycl  35273  cusgracyclt3v  35299  sumeq2si  36345  prodeq2si  36347  cbvprodvw2  36390  cos2h  37751  tan2h  37752  lhpocnel2  40218  cdlemk19w  41171  lcmineqlem  42245  rencldnfilem  43004  imsqrtvalex  43829  frege70  44116  frege118  44164  hashnzfzclim  44505  dvradcnv2  44530  binomcxplemnotnn0  44539  supxrleubrnmptf  45637  ioonct  45725  fourierdlem112  46404  salexct2  46525  addmodne  47532  m1modnep2mod  47540  difmodm1lt  47547  flsqrt5  47782  lighneallem4b  47797  fpprel2  47929  gbegt5  47949  gbowgt5  47950  gbowge7  47951  gbege6  47953  sbgoldbwt  47965  sbgoldbst  47966  sbgoldbalt  47969  sbgoldbm  47972  nnsum3primesle9  47982  nnsum4primesevenALTV  47989  bgoldbtbndlem1  47993  tgblthelfgott  48003  gpg3kgrtriexlem5  48275