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

Theorem eqbrtri 4830
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
eqbrtr.1 𝐴 = 𝐵
eqbrtr.2 𝐵𝑅𝐶
Assertion
Ref Expression
eqbrtri 𝐴𝑅𝐶

Proof of Theorem eqbrtri
StepHypRef Expression
1 eqbrtr.2 . 2 𝐵𝑅𝐶
2 eqbrtr.1 . . 3 𝐴 = 𝐵
32breq1i 4816 . 2 (𝐴𝑅𝐶𝐵𝑅𝐶)
41, 3mpbir 222 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652   class class class wbr 4809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810
This theorem is referenced by:  eqbrtrri  4832  3brtr4i  4839  infxpenc2  9096  pm110.643  9252  pwsdompw  9279  r1om  9319  aleph1  9646  canthp1lem1  9727  neg1lt0  11396  halflt1  11496  3halfnz  11703  declei  11777  numlti  11778  sqlecan  13178  discr  13208  faclbnd3  13283  hashunlei  13413  hashge2el2dif  13463  geo2lim  14892  0.999...  14898  geoihalfsum  14899  cos2bnd  15202  sin4lt0  15209  eirrlem  15216  rpnnen2lem3  15229  rpnnen2lem9  15235  aleph1re  15258  1nprm  15674  strle2  16248  strle3  16249  1strstr  16253  2strstr  16257  rngstr  16274  srngfn  16282  lmodstr  16291  ipsstr  16298  phlstr  16308  topgrpstr  16316  otpsstr  16323  odrngstr  16334  imasvalstr  16380  0frgp  18458  cnfldstr  20021  zlmlem  20138  tnglem  22723  iscmet3lem3  23367  mbfimaopnlem  23713  mbfsup  23722  mbfi1fseqlem6  23778  aalioulem3  24380  aaliou3lem3  24390  dvradcnv  24466  asin1  24912  log2cnv  24962  log2tlbnd  24963  mule1  25165  bposlem5  25304  bposlem8  25307  zabsle1  25312  trkgstr  25634  0pth  27361  ex-fl  27698  blocnilem  28050  norm3difi  28395  norm3adifii  28396  bcsiALT  28427  nmopsetn0  29115  nmfnsetn0  29128  nmopge0  29161  nmfnge0  29177  0bdop  29243  nmcexi  29276  opsqrlem6  29395  dp2lt10  29974  dplti  29995  dpmul4  30004  locfinref  30290  dya2iocct  30724  signswch  31021  hgt750lem  31112  hgt750lem2  31113  subfaclim  31550  logi  31997  faclim  32009  cnndvlem1  32899  taupilem2  33534  cntotbnd  33949  diophren  37987  algstr  38356  binomcxplemnn0  39154  binomcxplemrat  39155  stirlinglem1  40860  dirkercncflem1  40889  fouriersw  41017  meaiunlelem  41254  evengpoap3  42295  exple2lt6  42746  nnlog2ge0lt1  42961
  Copyright terms: Public domain W3C validator