MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3brtr4i Structured version   Visualization version   GIF version

Theorem 3brtr4i 4816
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
Hypotheses
Ref Expression
3brtr4.1 𝐴𝑅𝐵
3brtr4.2 𝐶 = 𝐴
3brtr4.3 𝐷 = 𝐵
Assertion
Ref Expression
3brtr4i 𝐶𝑅𝐷

Proof of Theorem 3brtr4i
StepHypRef Expression
1 3brtr4.2 . . 3 𝐶 = 𝐴
2 3brtr4.1 . . 3 𝐴𝑅𝐵
31, 2eqbrtri 4807 . 2 𝐶𝑅𝐵
4 3brtr4.3 . 2 𝐷 = 𝐵
53, 4breqtrri 4813 1 𝐶𝑅𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631   class class class wbr 4786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787
This theorem is referenced by:  1lt2nq  9997  0lt1sr  10118  declt  11732  decltOLD  11733  decltc  11734  decltcOLD  11735  decle  11742  decleOLD  11745  fzennn  12975  faclbnd4lem1  13284  fsumabs  14740  ovolfiniun  23489  log2ublem3  24896  log2ub  24897  emgt0  24954  bclbnd  25226  bposlem8  25237  baseltedgf  26093  nmblolbii  27994  normlem6  28312  norm-ii-i  28334  nmbdoplbi  29223  dp2lt  29932  dp2ltsuc  29933  dp2ltc  29934  dplt  29952  dpltc  29955  dpmul4  29962  hgt750lemd  31066  hgt750lem  31069  supxrltinfxr  40193  nnsum4primesevenALTV  42217
  Copyright terms: Public domain W3C validator