Theorem breqtrri 5176

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
breqtrr.1	⊢ 𝐴𝑅𝐵
breqtrr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrri	⊢ 𝐴𝑅𝐶

Proof of Theorem breqtrri

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2734	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtri 5174	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1533   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150

This theorem is referenced by:  3brtr4i  5179  ensn1  9042  ensn1OLD  9043  1sdom2ALT  9266  dju1p1e2ALT  10199  infmap2  10243  0lt1sr  11120  0le2  12347  2pos  12348  3pos  12350  4pos  12352  5pos  12354  6pos  12355  7pos  12356  8pos  12357  9pos  12358  1lt2  12416  2lt3  12417  3lt4  12419  4lt5  12422  5lt6  12426  6lt7  12431  7lt8  12437  8lt9  12444  nn0le2xi  12559  numltc  12736  declti  12748  xlemul1a  13302  sqge0i  14187  faclbnd2  14286  cats1fv  14846  ege2le3  16070  cos2bnd  16168  3dvdsdec  16312  n2dvdsm1  16349  sumeven  16367  divalglem2  16375  pockthi  16879  dec2dvds  17035  prmlem1  17080  prmlem2  17092  1259prm  17108  2503prm  17112  4001prm  17117  2strstr1OLD  17209  vitalilem5  25585  dveflem  25955  tangtx  26485  sinq12ge0  26488  logi  26566  cxpge0  26662  asin1  26871  birthday  26931  lgamgulmlem4  27009  ppiub  27182  bposlem7  27268  lgsdir2lem2  27304  n0scut  28255  pthdlem2  29654  ex-fl  30329  ex-ind-dvds  30343  siilem2  30734  normlem6  30997  normlem7  30998  cm2mi  31508  pjnormi  31603  unierri  31986  dp2lt10  32692  dpgti  32714  pfx1s2  32749  cyc2fv2  32935  cyc3fv3  32952  hgt750lemd  34411  hgt750lem  34414  hgt750lem2  34415  hgt750leme  34421  cnndvlem1  36143  taupi  36933  poimirlem25  37249  poimirlem26  37250  poimirlem27  37251  poimirlem28  37252  ftc1anclem5  37301  fdc  37349  lcmineqlem23  41654  3lexlogpow2ineq2  41662  pellfundgt1  42445  jm2.27dlem2  42573  stoweidlem13  45539  sqwvfoura  45754  sqwvfourb  45755  fourierswlem  45756  tworepnotupword  46410  41prothprm  47096  tgblthelfgott  47292  tgoldbachlt  47293  nnlog2ge0lt1  47825  1aryenefmnd  47905  ackval42  47955

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »