Theorem breq1i 5114

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  eqbrtri  5128  brtpos0  8212  brtpos  8214  euen1  8998  euen1b  8999  2dom  9001  0sdom1domALT  9186  1sdom2  9187  modom2  9192  1sdomOLD  9196  infglb  9442  infglbb  9443  cnfcom3lem  9656  pr2nelemOLD  9956  axdclem2  10473  rnct  10478  cfpwsdom  10537  inar1  10728  reclem3pr  11002  gt0srpr  11031  mappsrpr  11061  ltpsrpr  11062  map2psrpr  11063  axpre-mulgt0  11121  lt0neg1  11684  le0neg1  11686  reclt1  12078  addltmul  12418  eluz2b1  12878  xlt0neg1  13179  xle0neg1  13181  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  elfznelfzo  13733  bernneq  14194  nn0opthlem1  14233  faclbnd4lem1  14258  hashge0  14352  hashgt23el  14389  hashge2el2difr  14446  cbvsum  15661  divcnvshft  15821  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  iprodmul  15969  oddge22np1  16319  nn0o1gt2  16351  divalglem1  16364  divalglem6  16368  isprm3  16653  dvdsnprmd  16660  2mulprm  16663  ge2nprmge4  16671  prmgaplem3  17024  isnzr2  20427  chrdvds  21436  chrcong  21437  lindsmm  21737  cpmidpmat  22760  csdfil  23781  iscau3  25178  ioombl1lem4  25462  itg2cn  25664  radcnvlt1  26327  sincosq1sgn  26407  sincosq3sgn  26409  sincosq4sgn  26410  ang180lem3  26721  leibpilem2  26851  issqf  27046  bposlem6  27200  gausslemma2dlem3  27279  nosupinfsep  27644  addscut  27885  mulscut  28035  mulscan2d  28082  recsex  28121  abssneg  28149  clwlkclwwlklem2  29929  clwlkclwwlk2  29932  clwlkclwwlkf  29937  clwlknf1oclwwlknlem1  30010  konigsberglem5  30185  cvexchi  32298  addltmulALT  32375  xnn01gt  32693  dya2iocct  34271  ballotlemi1  34494  signswch  34552  usgrgt2cycl  35117  cusgracyclt3v  35143  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  cos2h  37605  tan2h  37606  lhpocnel2  40013  cdlemk19w  40966  lcmineqlem  42040  rencldnfilem  42808  imsqrtvalex  43635  frege70  43922  frege118  43970  hashnzfzclim  44311  dvradcnv2  44336  binomcxplemnotnn0  44345  supxrleubrnmptf  45447  ioonct  45535  fourierdlem112  46216  salexct2  46337  addmodne  47345  m1modnep2mod  47353  difmodm1lt  47360  flsqrt5  47595  lighneallem4b  47610  fpprel2  47742  gbegt5  47762  gbowgt5  47763  gbowge7  47764  gbege6  47766  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbalt  47782  sbgoldbm  47785  nnsum3primesle9  47795  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  tgblthelfgott  47816  gpg3kgrtriexlem5  48078