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

Theorem eqbrtrrd 4061
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 2301 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 4059 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  dftpos4  6269  fodomfi  7151  cnfcom2lem  7420  infcda1  7835  enfin1ai  8026  fin56  8035  pwcfsdom  8221  fpwwe2lem7  8274  fpwwe2  8281  canthp1lem1  8290  1nqenq  8602  prlem936  8687  lemulge11  9634  supmul1  9735  xaddge0  10594  xadddi2  10633  ltexp2a  11169  leexp2a  11173  nnlesq  11222  digit1  11251  faclbnd4lem1  11322  faclbnd6  11328  facavg  11330  abs3dif  11831  abs2dif  11832  limsupgre  11971  rlimclim1  12035  rlimuni  12040  rlimres2  12051  rlimcn1  12078  rlimcn1b  12079  recn2  12090  imcn2  12091  rlimo1  12106  o1rlimmul  12108  iserex  12146  isercoll  12157  caucvgrlem2  12163  caucvgr  12164  iseraltlem3  12172  summolem2a  12204  fsumge1  12271  o1fsum  12287  isumrpcl  12318  climcnds  12326  harmonic  12333  mertenslem1  12356  ege2le3  12387  efgt1p2  12410  efgt1p  12411  eirrlem  12498  rpnnen2lem11  12519  fsumdvds  12588  bitsfzo  12642  bitsmod  12643  bitscmp  12645  mulgcd  12741  dvdssqlem  12754  nn0seqcvgd  12756  mulgcddvds  12799  rpdvds  12819  qden1elz  12844  phimullem  12863  pcdvdstr  12944  pockthg  12969  prmreclem1  12979  4sqlem11  13018  ramub1lem1  13089  ramub1lem2  13090  mreexexlem4d  13565  sscid  13717  latmlej21  14214  latmlej22  14215  lubel  14242  efginvrel1  15053  odadd2  15157  odadd  15158  gexexlem  15160  cyggex2  15199  ablfacrplem  15316  ablfac1c  15322  ablfac1eu  15324  pgpfac1lem3a  15327  isabvd  15601  znrrg  16535  lmcn2  17359  metrtri  17937  imasdsf1olem  17953  stdbdxmet  18077  nrmmetd  18113  nmmtri  18159  nlmvscnlem2  18212  blcvx  18320  recld2  18336  zdis  18338  opnreen  18352  cnheibor  18469  lebnumlem3  18477  nmoleub2lem3  18612  nmoleub2lem2  18613  nmoleub3  18616  ipcnlem2  18687  cmetcaulem  18730  cncmet  18760  minveclem4  18812  ovoliunlem1  18877  ovoliun2  18881  ovolscalem1  18888  ovolicopnf  18899  voliunlem2  18924  volsup  18929  ioorcl2  18943  uniiccvol  18951  uniioombllem4  18957  i1fd  19052  mbfi1fseqlem4  19089  itg2const2  19112  itg2eqa  19116  itg2split  19120  itg2i1fseqle  19125  itg2cnlem2  19133  dvcnv  19340  dveflem  19342  dvferm1lem  19347  dvlip2  19358  c1liplem1  19359  dvivthlem1  19371  lhop1lem  19376  dvcvx  19383  dvfsumle  19384  dvfsumabs  19386  dvfsumlem4  19392  dvfsumrlim2  19395  ftc1a  19400  deg1pwle  19521  fta1blem  19570  aalioulem3  19730  aaliou2b  19737  ulmbdd  19791  ulmdvlem1  19793  itgulm  19800  pserdvlem2  19820  abelthlem3  19825  abelthlem5  19827  abelthlem6  19828  abelthlem7  19830  tanregt0  19917  argimlt0  19983  logdivlti  19987  logcnlem3  20007  logcnlem4  20008  logtayl  20023  logtayl2  20025  cxple2  20060  cxpcn3lem  20103  cxpaddle  20108  isosctrlem1  20134  atantayl  20249  efrlim  20280  dfef2  20281  o1cxp  20285  cxp2lim  20287  divsqrsumo1  20294  amgmlem  20300  logdifbnd  20304  emcllem7  20311  harmonicbnd4  20320  fsumharmonic  20321  ftalem2  20327  basellem2  20335  basellem5  20338  basellem9  20342  vma1  20420  sqff1o  20436  fsumfldivdiaglem  20445  chtub  20467  fsumvma2  20469  chpchtsum  20474  chpub  20475  logfaclbnd  20477  logfacbnd3  20478  logfacrlim  20479  logexprlim  20480  bcmono  20532  bposlem2  20540  bposlem5  20543  bposlem6  20544  lgsne0  20588  lgsquadlem1  20609  lgsquadlem2  20610  2sqblem  20632  chebbnd1lem1  20634  chtppilimlem1  20638  chtppilimlem2  20639  chpchtlim  20644  rplogsumlem1  20649  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0fno1  20676  dchrisum0re  20678  dchrisum0lem2a  20682  dchrisum0lem3  20684  dirith  20694  mulog2sumlem1  20699  mulog2sumlem2  20700  log2sumbnd  20709  selberglem2  20711  logdivbnd  20721  selberg3lem1  20722  selberg4lem1  20725  pntrsumbnd2  20732  pntrlog2bndlem1  20742  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntibndlem3  20757  pntlemb  20762  pntlemn  20765  pntlemr  20767  pntlemj  20768  pntlemf  20770  pntlemo  20772  ostth2lem3  20800  ostth3  20803  nvabs  21255  nvlmle  21281  smcnlem  21286  ubthlem2  21466  minvecolem4  21475  htthlem  21513  normpyc  21741  nmophmi  22627  hstle  22826  hstles  22827  stlei  22836  xrge0npcan  23348  esumpinfval  23456  esumpinfsum  23460  dya2iocseg  23594  rescon  23792  sinccvglem  24020  circum  24022  prodmolem2a  24157  btwnxfr  24751  supaddc  24995  itg2addnc  25005  mslb1  25710  supnufb  25733  nn0prpwlem  26341  csbrn  26565  trirn  26566  isbnd3  26611  cntotbnd  26623  bfp  26651  rrndstprj2  26658  irrapxlem1  27010  irrapxlem4  27013  pell1qrgaplem  27061  pellfundglb  27073  rmspecfund  27097  monotoddzzfi  27130  rmynn  27146  jm2.24nn  27149  jm2.17c  27152  jm2.24  27153  acongeq  27173  jm2.20nn  27193  jm2.26lem3  27197  jm2.27a  27201  jm2.27c  27203  rmydioph  27210  jm3.1lem2  27214  frlmpwfi  27365  f1linds  27398  hashgcdlem  27619  hashgcdeq  27620  cncmpmax  27806  fmul01lt1lem2  27818  clim1fr1  27830  stoweidlem1  27853  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem24  27876  stoweidlem26  27878  stoweidlem38  27890  stoweidlem44  27896  wallispilem4  27920  wallispilem5  27921  stirlinglem11  27936  1cvrjat  30286  3atlem1  30294  3atlem6  30299  llnmlplnN  30350  2llnjaN  30377  2lplnja  30430  dalem57  30540  dalawlem11  30692  dalawlem12  30693  lhp2lt  30812  lhpj1  30833  lhpm0atN  30840  4atexlemex2  30882  lautm  30905  cdleme17b  31098  cdleme20j  31129  cdleme30a  31189  cdlemg4c  31423  cdlemg17a  31472  cdlemg31c  31510  trljco  31551  cdlemk46  31759  dia2dimlem2  31877  cdlemm10N  31930  cdlemn10  32018  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem15N  32133  mapdat  32479
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