MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqtrri Unicode version

Theorem breqtrri 4477
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
StepHypRef Expression
1 breqtrr.1 . 2
2 breqtrr.2 . . 3
32eqcomi 2470 . 2
41, 3breqtri 4475 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  3brtr4i  4480  ensn1  7599  1sdom2  7738  pm110.643ALT  8579  infmap2  8619  0lt1sr  9493  0le2  10651  2pos  10652  3pos  10654  4pos  10656  5pos  10658  6pos  10659  7pos  10660  8pos  10661  9pos  10662  10pos  10663  1lt2  10727  2lt3  10728  3lt4  10730  4lt5  10733  5lt6  10737  6lt7  10742  7lt8  10748  8lt9  10755  9lt10  10763  nn0le2xi  10872  numltc  11024  declti  11029  xlemul1a  11509  sqge0i  12255  faclbnd2  12369  cats1fv  12824  ege2le3  13825  cos2bnd  13923  divalglem2  14053  pockthi  14425  dec2dvds  14549  prmlem1  14593  prmlem2  14605  1259prm  14618  2503prm  14622  4001prm  14627  vitalilem5  22021  dveflem  22380  tangtx  22898  sinq12ge0  22901  cxpge0  23064  asin1  23225  birthday  23284  ppiub  23479  bposlem4  23562  bposlem5  23563  bposlem7  23565  lgsdir2lem2  23599  ex-fl  25168  ex-ind-dvds  25170  siilem2  25767  normlem6  26032  normlem7  26033  cm2mi  26544  pjnormi  26639  unierri  27023  lgamgulmlem4  28574  logi  29121  ftc1anclem5  30094  fdc  30238  pellfundgt1  30819  jm2.27dlem2  30952  stoweidlem13  31795  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  taupi  37698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator