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

Theorem eqbrtrrd 4045
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1  |-  ( ph  ->  A  =  B )
eqbrtrrd.2  |-  ( ph  ->  A R C )
Assertion
Ref Expression
eqbrtrrd  |-  ( ph  ->  B R C )

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2288 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 4043 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  dftpos4  6253  fodomfi  7135  cnfcom2lem  7404  infcda1  7819  enfin1ai  8010  fin56  8019  pwcfsdom  8205  fpwwe2lem7  8258  fpwwe2  8265  canthp1lem1  8274  1nqenq  8586  prlem936  8671  lemulge11  9618  supmul1  9719  xaddge0  10578  xadddi2  10617  ltexp2a  11153  leexp2a  11157  nnlesq  11206  digit1  11235  faclbnd4lem1  11306  faclbnd6  11312  facavg  11314  abs3dif  11815  abs2dif  11816  limsupgre  11955  rlimclim1  12019  rlimuni  12024  rlimres2  12035  rlimcn1  12062  rlimcn1b  12063  recn2  12074  imcn2  12075  rlimo1  12090  o1rlimmul  12092  iserex  12130  isercoll  12141  caucvgrlem2  12147  caucvgr  12148  iseraltlem3  12156  summolem2a  12188  fsumge1  12255  o1fsum  12271  isumrpcl  12302  climcnds  12310  harmonic  12317  mertenslem1  12340  ege2le3  12371  efgt1p2  12394  efgt1p  12395  eirrlem  12482  rpnnen2lem11  12503  fsumdvds  12572  bitsfzo  12626  bitsmod  12627  bitscmp  12629  mulgcd  12725  dvdssqlem  12738  nn0seqcvgd  12740  mulgcddvds  12783  rpdvds  12803  qden1elz  12828  phimullem  12847  pcdvdstr  12928  pockthg  12953  prmreclem1  12963  4sqlem11  13002  ramub1lem1  13073  ramub1lem2  13074  mreexexlem4d  13549  sscid  13701  latmlej21  14198  latmlej22  14199  lubel  14226  efginvrel1  15037  odadd2  15141  odadd  15142  gexexlem  15144  cyggex2  15183  ablfacrplem  15300  ablfac1c  15306  ablfac1eu  15308  pgpfac1lem3a  15311  isabvd  15585  znrrg  16519  lmcn2  17343  metrtri  17921  imasdsf1olem  17937  stdbdxmet  18061  nrmmetd  18097  nmmtri  18143  nlmvscnlem2  18196  blcvx  18304  recld2  18320  zdis  18322  opnreen  18336  cnheibor  18453  lebnumlem3  18461  nmoleub2lem3  18596  nmoleub2lem2  18597  nmoleub3  18600  ipcnlem2  18671  cmetcaulem  18714  cncmet  18744  minveclem4  18796  ovoliunlem1  18861  ovoliun2  18865  ovolscalem1  18872  ovolicopnf  18883  voliunlem2  18908  volsup  18913  ioorcl2  18927  uniiccvol  18935  uniioombllem4  18941  i1fd  19036  mbfi1fseqlem4  19073  itg2const2  19096  itg2eqa  19100  itg2split  19104  itg2i1fseqle  19109  itg2cnlem2  19117  dvcnv  19324  dveflem  19326  dvferm1lem  19331  dvlip2  19342  c1liplem1  19343  dvivthlem1  19355  lhop1lem  19360  dvcvx  19367  dvfsumle  19368  dvfsumabs  19370  dvfsumlem4  19376  dvfsumrlim2  19379  ftc1a  19384  deg1pwle  19505  fta1blem  19554  aalioulem3  19714  aaliou2b  19721  ulmbdd  19775  ulmdvlem1  19777  itgulm  19784  pserdvlem2  19804  abelthlem3  19809  abelthlem5  19811  abelthlem6  19812  abelthlem7  19814  tanregt0  19901  argimlt0  19967  logdivlti  19971  logcnlem3  19991  logcnlem4  19992  logtayl  20007  logtayl2  20009  cxple2  20044  cxpcn3lem  20087  cxpaddle  20092  isosctrlem1  20118  atantayl  20233  efrlim  20264  dfef2  20265  o1cxp  20269  cxp2lim  20271  divsqrsumo1  20278  amgmlem  20284  logdifbnd  20288  emcllem7  20295  harmonicbnd4  20304  fsumharmonic  20305  ftalem2  20311  basellem2  20319  basellem5  20322  basellem9  20326  vma1  20404  sqff1o  20420  fsumfldivdiaglem  20429  chtub  20451  fsumvma2  20453  chpchtsum  20458  chpub  20459  logfaclbnd  20461  logfacbnd3  20462  logfacrlim  20463  logexprlim  20464  bcmono  20516  bposlem2  20524  bposlem5  20527  bposlem6  20528  lgsne0  20572  lgsquadlem1  20593  lgsquadlem2  20594  2sqblem  20616  chebbnd1lem1  20618  chtppilimlem1  20622  chtppilimlem2  20623  chpchtlim  20628  rplogsumlem1  20633  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lem2a  20666  dchrisum0lem3  20668  dirith  20678  mulog2sumlem1  20683  mulog2sumlem2  20684  log2sumbnd  20693  selberglem2  20695  logdivbnd  20705  selberg3lem1  20706  selberg4lem1  20709  pntrsumbnd2  20716  pntrlog2bndlem1  20726  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem3  20741  pntlemb  20746  pntlemn  20749  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemo  20756  ostth2lem3  20784  ostth3  20787  nvabs  21239  nvlmle  21265  smcnlem  21270  ubthlem2  21450  minvecolem4  21459  htthlem  21497  normpyc  21725  nmophmi  22611  hstle  22810  hstles  22811  stlei  22820  xrge0npcan  23333  esumpinfval  23441  esumpinfsum  23445  dya2iocseg  23579  rescon  23777  sinccvglem  24005  circum  24007  btwnxfr  24679  mslb1  25607  supnufb  25630  nn0prpwlem  26238  csbrn  26462  trirn  26463  isbnd3  26508  cntotbnd  26520  bfp  26548  rrndstprj2  26555  irrapxlem1  26907  irrapxlem4  26910  pell1qrgaplem  26958  pellfundglb  26970  rmspecfund  26994  monotoddzzfi  27027  rmynn  27043  jm2.24nn  27046  jm2.17c  27049  jm2.24  27050  acongeq  27070  jm2.20nn  27090  jm2.26lem3  27094  jm2.27a  27098  jm2.27c  27100  rmydioph  27107  jm3.1lem2  27111  frlmpwfi  27262  f1linds  27295  hashgcdlem  27516  hashgcdeq  27517  cncmpmax  27703  fmul01lt1lem2  27715  clim1fr1  27727  stoweidlem1  27750  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem24  27773  stoweidlem26  27775  stoweidlem38  27787  stoweidlem44  27793  wallispilem4  27817  wallispilem5  27818  stirlinglem11  27833  1cvrjat  29664  3atlem1  29672  3atlem6  29677  llnmlplnN  29728  2llnjaN  29755  2lplnja  29808  dalem57  29918  dalawlem11  30070  dalawlem12  30071  lhp2lt  30190  lhpj1  30211  lhpm0atN  30218  4atexlemex2  30260  lautm  30283  cdleme17b  30476  cdleme20j  30507  cdleme30a  30567  cdlemg4c  30801  cdlemg17a  30850  cdlemg31c  30888  trljco  30929  cdlemk46  31137  dia2dimlem2  31255  cdlemm10N  31308  cdlemn10  31396  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem15N  31511  mapdat  31857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator