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

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

Proof of Theorem eqbrtrri
StepHypRef Expression
1 eqbrtrr.1 . . 3  |-  A  =  B
21eqcomi 2437 . 2  |-  B  =  A
3 eqbrtrr.2 . 2  |-  A R C
42, 3eqbrtri 4299 1  |-  B R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  3brtr3i  4307  expnass  11954  faclbnd4lem1  12052  sqr2gt1lt2  12747  cos1bnd  13453  cos2bnd  13454  prdsvalstr  14373  ovolre  20849  pige3  21863  atan1  22207  log2ublem1  22225  sqrlim  22250  bposlem8  22514  chebbnd1  22605  konigsberg  23430  norm-ii-i  24361  nmopadji  25316  unierri  25330  ballotlem2  26718  stoweidlem26  29664  wallispilem5  29707
  Copyright terms: Public domain W3C validator