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

Theorem eqbrtri 4058
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqbrtr.1  |-  A  =  B
eqbrtr.2  |-  B R C
Assertion
Ref Expression
eqbrtri  |-  A R C

Proof of Theorem eqbrtri
StepHypRef Expression
1 eqbrtr.2 . 2  |-  B R C
2 eqbrtr.1 . . 3  |-  A  =  B
32breq1i 4046 . 2  |-  ( A R C  <->  B R C )
41, 3mpbir 200 1  |-  A R C
Colors of variables: wff set class
Syntax hints:    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  eqbrtrri  4060  3brtr4i  4067  infxpenc2  7665  pm110.643  7819  pwsdompw  7846  r1om  7886  aleph1  8209  canthp1lem1  8290  pwxpndom2  8303  halflt1  9949  numlti  10164  sqlecan  11225  discr  11254  faclbnd3  11321  hashunlei  11393  geo2lim  12347  0.999...  12353  geoihalfsum  12354  cos2bnd  12484  sin4lt0  12491  eirrlem  12498  rpnnen2lem3  12511  rpnnen2lem9  12517  aleph1re  12539  nthruz  12546  1nprm  12779  163prm  13142  631prm  13144  strle2  13256  strle3  13257  2strstr  13260  rngstr  13271  srngfn  13279  lmodstr  13288  algstr  13293  phlstr  13303  topgrpstr  13311  otpsstr  13318  odrngstr  13327  imasvalstr  13368  ipostr  14272  0frgp  15104  cnfldstr  16395  zlmlem  16487  thlle  16613  tnglem  18172  iscmet3lem3  18732  mbfimaopnlem  19026  mbfsup  19035  mbfi1fseqlem6  19091  aalioulem3  19730  aaliou3lem3  19740  dvradcnv  19813  asin1  20206  log2cnv  20256  log2tlbnd  20257  mule1  20402  bposlem5  20543  bposlem8  20546  ex-fl  20850  blocnilem  21398  norm3difi  21742  norm3adifii  21743  bcsiALT  21774  nmopsetn0  22461  nmfnsetn0  22474  nmopge0  22507  nmfnge0  22523  0bdop  22589  nmcexi  22622  opsqrlem6  22741  subfaclim  23734  faclimlem3  24119  cntotbnd  26623  diophren  26999  wallispi2  27925  stirlinglem1  27926  0pth  28356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator