Theorem breq1i 5116

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

Syntax hints:   ↔ wb 209   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  eqbrtri  5132  brtpos0  8225  brtpos  8227  euen1  9020  euen1b  9021  2dom  9023  0sdom1domALT  9203  1sdom2  9204  modom2  9208  infglb  9447  infglbb  9448  cnfcom3lem  9668  axdclem2  10499  rnct  10504  cfpwsdom  10564  inar1  10755  reclem3pr  11029  gt0srpr  11058  mappsrpr  11088  ltpsrpr  11089  map2psrpr  11090  axpre-mulgt0  11148  lt0neg1  11715  le0neg1  11717  reclt1  12105  addltmul  12475  eluz2b1  12938  xlt0neg1  13240  xle0neg1  13242  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  elfznelfzo  13798  bernneq  14261  nn0opthlem1  14300  faclbnd4lem1  14325  hashge0  14419  hashgt23el  14457  hashge2el2difr  14514  cbvsum  15742  divcnvshft  15905  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  iprodmul  16053  oddge22np1  16402  nn0o1gt2  16434  divalglem1  16447  divalglem6  16451  isprm3  16736  dvdsnprmd  16743  2mulprm  16746  ge2nprmge4  16755  prmgaplem3  17108  isnzr2  20615  chrdvds  21676  chrcong  21677  lindsmm  21978  cpmidpmat  23030  csdfil  24051  iscau3  25437  ioombl1lem4  25720  itg2cn  25922  radcnvlt1  26581  sincosq1sgn  26663  sincosq3sgn  26665  sincosq4sgn  26666  ang180lem3  26976  leibpilem2  27106  issqf  27300  bposlem6  27453  gausslemma2dlem3  27532  nosupinfsep  27896  addcuts  28171  mulcut  28325  mulscan2d  28372  recsex  28412  absnegs  28440  avglts1d  28646  avglts2d  28647  z12bdaylem1  28663  z12bday  28678  bdayfin  28680  clwlkclwwlklem2  30351  clwlkclwwlk2  30354  clwlkclwwlkf  30359  clwlknf1oclwwlknlem1  30432  konigsberglem5  30607  cvexchi  32721  addltmulALT  32798  xnn01gt  33115  dya2iocct  34670  ballotlemi1  34893  signswch  34948  usgrgt2cycl  35622  cusgracyclt3v  35648  sumeq2si  36734  prodeq2si  36736  cbvprodvw2  36779  cos2h  38282  tan2h  38283  lhpocnel2  40813  cdlemk19w  41766  lcmineqlem  42839  rencldnfilem  43567  imsqrtvalex  44392  frege70  44679  frege118  44727  hashnzfzclim  45052  dvradcnv2  45077  binomcxplemnotnn0  45086  supxrleubrnmptf  46185  ioonct  46273  fourierdlem112  46952  salexct2  47073  addmodne  48107  m1modnep2mod  48115  difmodm1lt  48122  2timesltsq  48135  2timesltsqm1  48136  flsqrt5  48366  lighneallem4b  48381  fpprel2  48526  gbegt5  48546  gbowgt5  48547  gbowge7  48548  gbege6  48550  sbgoldbwt  48562  sbgoldbst  48563  sbgoldbalt  48566  sbgoldbm  48569  nnsum3primesle9  48579  nnsum4primesevenALTV  48586  bgoldbtbndlem1  48590  tgblthelfgott  48600  gpg3kgrtriexlem5  48872