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

Theorem eqbrtri 4231
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 4219 . 2  |-  ( A R C  <->  B R C )
41, 3mpbir 201 1  |-  A R C
Colors of variables: wff set class
Syntax hints:    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  eqbrtrri  4233  3brtr4i  4240  infxpenc2  7903  pm110.643  8057  pwsdompw  8084  r1om  8124  aleph1  8446  canthp1lem1  8527  pwxpndom2  8540  halflt1  10189  numlti  10406  sqlecan  11487  discr  11516  faclbnd3  11583  hashunlei  11684  geo2lim  12652  0.999...  12658  geoihalfsum  12659  cos2bnd  12789  sin4lt0  12796  eirrlem  12803  rpnnen2lem3  12816  rpnnen2lem9  12822  aleph1re  12844  nthruz  12851  1nprm  13084  163prm  13447  631prm  13449  strle2  13561  strle3  13562  2strstr  13565  rngstr  13576  srngfn  13584  lmodstr  13593  algstr  13598  phlstr  13608  topgrpstr  13616  otpsstr  13623  odrngstr  13634  imasvalstr  13675  ipostr  14579  0frgp  15411  cnfldstr  16705  zlmlem  16798  thlle  16924  tnglem  18681  iscmet3lem3  19243  mbfimaopnlem  19547  mbfsup  19556  mbfi1fseqlem6  19612  aalioulem3  20251  aaliou3lem3  20261  dvradcnv  20337  asin1  20734  log2cnv  20784  log2tlbnd  20785  mule1  20931  bposlem5  21072  bposlem8  21075  0pth  21570  ex-fl  21755  blocnilem  22305  norm3difi  22649  norm3adifii  22650  bcsiALT  22681  nmopsetn0  23368  nmfnsetn0  23381  nmopge0  23414  nmfnge0  23430  0bdop  23496  nmcexi  23529  opsqrlem6  23648  dya2iocct  24630  subfaclim  24874  faclim  25365  cntotbnd  26505  diophren  26874  stirlinglem1  27799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator