Theorem breq1i 5105

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  eqbrtri  5119  brtpos0  8175  brtpos  8177  euen1  8966  euen1b  8967  2dom  8969  0sdom1domALT  9149  1sdom2  9150  modom2  9154  infglb  9396  infglbb  9397  cnfcom3lem  9614  axdclem2  10432  rnct  10437  cfpwsdom  10497  inar1  10688  reclem3pr  10962  gt0srpr  10991  mappsrpr  11021  ltpsrpr  11022  map2psrpr  11023  axpre-mulgt0  11081  lt0neg1  11645  le0neg1  11647  reclt1  12039  addltmul  12379  eluz2b1  12834  xlt0neg1  13136  xle0neg1  13138  iccshftr  13404  iccshftl  13406  iccdil  13408  icccntr  13410  elfznelfzo  13691  bernneq  14154  nn0opthlem1  14193  faclbnd4lem1  14218  hashge0  14312  hashgt23el  14349  hashge2el2difr  14406  cbvsum  15620  divcnvshft  15780  cbvprod  15838  cbvprodv  15839  prodeq1i  15841  iprodmul  15928  oddge22np1  16278  nn0o1gt2  16310  divalglem1  16323  divalglem6  16327  isprm3  16612  dvdsnprmd  16619  2mulprm  16622  ge2nprmge4  16630  prmgaplem3  16983  isnzr2  20453  chrdvds  21483  chrcong  21484  lindsmm  21785  cpmidpmat  22819  csdfil  23840  iscau3  25236  ioombl1lem4  25520  itg2cn  25722  radcnvlt1  26385  sincosq1sgn  26465  sincosq3sgn  26467  sincosq4sgn  26468  ang180lem3  26779  leibpilem2  26909  issqf  27104  bposlem6  27258  gausslemma2dlem3  27337  nosupinfsep  27702  addcuts  27976  mulcut  28130  mulscan2d  28177  recsex  28217  absnegs  28245  avglts1d  28451  avglts2d  28452  z12bdaylem1  28468  z12bday  28483  bdayfin  28485  clwlkclwwlklem2  30077  clwlkclwwlk2  30080  clwlkclwwlkf  30085  clwlknf1oclwwlknlem1  30158  konigsberglem5  30333  cvexchi  32446  addltmulALT  32523  xnn01gt  32852  dya2iocct  34439  ballotlemi1  34662  signswch  34720  usgrgt2cycl  35326  cusgracyclt3v  35352  sumeq2si  36398  prodeq2si  36400  cbvprodvw2  36443  cos2h  37814  tan2h  37815  lhpocnel2  40301  cdlemk19w  41254  lcmineqlem  42328  rencldnfilem  43083  imsqrtvalex  43908  frege70  44195  frege118  44243  hashnzfzclim  44584  dvradcnv2  44609  binomcxplemnotnn0  44618  supxrleubrnmptf  45716  ioonct  45804  fourierdlem112  46483  salexct2  46604  addmodne  47611  m1modnep2mod  47619  difmodm1lt  47626  flsqrt5  47861  lighneallem4b  47876  fpprel2  48008  gbegt5  48028  gbowgt5  48029  gbowge7  48030  gbege6  48032  sbgoldbwt  48044  sbgoldbst  48045  sbgoldbalt  48048  sbgoldbm  48051  nnsum3primesle9  48061  nnsum4primesevenALTV  48068  bgoldbtbndlem1  48072  tgblthelfgott  48082  gpg3kgrtriexlem5  48354