Theorem breq1i 5155

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

Syntax hints:   ↔ wb 205   = wceq 1542   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  eqbrtri  5169  brtpos0  8215  brtpos  8217  euen1  9023  euen1b  9024  2dom  9027  0sdom1domALT  9236  1sdom2  9237  modom2  9242  1sdomOLD  9246  infglb  9482  infglbb  9483  cnfcom3lem  9695  pr2nelemOLD  9995  axdclem2  10512  rnct  10517  cfpwsdom  10576  inar1  10767  reclem3pr  11041  gt0srpr  11070  mappsrpr  11100  ltpsrpr  11101  map2psrpr  11102  axpre-mulgt0  11160  lt0neg1  11717  le0neg1  11719  reclt1  12106  addltmul  12445  eluz2b1  12900  xlt0neg1  13195  xle0neg1  13197  iccshftr  13460  iccshftl  13462  iccdil  13464  icccntr  13466  elfznelfzo  13734  bernneq  14189  nn0opthlem1  14225  faclbnd4lem1  14250  hashge0  14344  hashgt23el  14381  hashge2el2difr  14439  cbvsum  15638  divcnvshft  15798  cbvprod  15856  iprodmul  15944  oddge22np1  16289  nn0o1gt2  16321  divalglem1  16334  divalglem6  16338  isprm3  16617  dvdsnprmd  16624  2mulprm  16627  ge2nprmge4  16635  prmgaplem3  16983  isnzr2  20290  chrdvds  21072  chrcong  21073  lindsmm  21375  cpmidpmat  22367  csdfil  23390  iscau3  24787  ioombl1lem4  25070  itg2cn  25273  radcnvlt1  25922  sincosq1sgn  26000  sincosq3sgn  26002  sincosq4sgn  26003  ang180lem3  26306  leibpilem2  26436  issqf  26630  bposlem6  26782  gausslemma2dlem3  26861  nosupinfsep  27225  addscut  27452  mulscut  27578  mulscan2d  27621  recsex  27655  clwlkclwwlklem2  29243  clwlkclwwlk2  29246  clwlkclwwlkf  29251  clwlknf1oclwwlknlem1  29324  konigsberglem5  29499  cvexchi  31610  addltmulALT  31687  xnn01gt  31971  dya2iocct  33268  ballotlemi1  33490  signswch  33561  usgrgt2cycl  34110  cusgracyclt3v  34136  cos2h  36468  tan2h  36469  lhpocnel2  38879  cdlemk19w  39832  lcmineqlem  40906  rencldnfilem  41544  imsqrtvalex  42383  frege70  42670  frege118  42718  hashnzfzclim  43067  dvradcnv2  43092  binomcxplemnotnn0  43101  supxrleubrnmptf  44148  ioonct  44237  fourierdlem112  44921  salexct2  45042  flsqrt5  46249  lighneallem4b  46264  fpprel2  46396  gbegt5  46416  gbowgt5  46417  gbowge7  46418  gbege6  46420  sbgoldbwt  46432  sbgoldbst  46433  sbgoldbalt  46436  sbgoldbm  46439  nnsum3primesle9  46449  nnsum4primesevenALTV  46456  bgoldbtbndlem1  46460  tgblthelfgott  46470  difmodm1lt  47162