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

Theorem eqbrtrrd 4194
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 2409 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 4192 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  dftpos4  6457  fodomfi  7344  cnfcom2lem  7614  infcda1  8029  enfin1ai  8220  fin56  8229  pwcfsdom  8414  fpwwe2lem7  8467  fpwwe2  8474  canthp1lem1  8483  1nqenq  8795  prlem936  8880  lemulge11  9828  supmul1  9929  xaddge0  10793  xadddi2  10832  ltexp2a  11386  leexp2a  11390  nnlesq  11439  digit1  11468  faclbnd4lem1  11539  faclbnd6  11545  facavg  11547  abs3dif  12090  abs2dif  12091  limsupgre  12230  rlimclim1  12294  rlimuni  12299  rlimres2  12310  rlimcn1  12337  rlimcn1b  12338  recn2  12349  imcn2  12350  rlimo1  12365  o1rlimmul  12367  iserex  12405  isercoll  12416  caucvgrlem2  12423  caucvgr  12424  iseraltlem3  12432  summolem2a  12464  fsumge1  12531  o1fsum  12547  isumrpcl  12578  climcnds  12586  harmonic  12593  mertenslem1  12616  ege2le3  12647  efgt1p2  12670  efgt1p  12671  eirrlem  12758  rpnnen2lem11  12779  fsumdvds  12848  bitsfzo  12902  bitsmod  12903  bitscmp  12905  mulgcd  13001  dvdssqlem  13014  nn0seqcvgd  13016  mulgcddvds  13059  rpdvds  13079  qden1elz  13104  phimullem  13123  pcdvdstr  13204  pockthg  13229  prmreclem1  13239  4sqlem11  13278  ramub1lem1  13349  ramub1lem2  13350  mreexexlem4d  13827  sscid  13979  latmlej21  14476  latmlej22  14477  lubel  14504  efginvrel1  15315  odadd2  15419  odadd  15420  gexexlem  15422  cyggex2  15461  ablfacrplem  15578  ablfac1c  15584  ablfac1eu  15586  pgpfac1lem3a  15589  isabvd  15863  znrrg  16801  lmcn2  17634  metrtri  18340  imasdsf1olem  18356  stdbdxmet  18498  nrmmetd  18575  nmmtri  18621  nlmvscnlem2  18674  blcvx  18782  recld2  18798  zdis  18800  opnreen  18815  cnheibor  18933  lebnumlem3  18941  nmoleub2lem3  19076  nmoleub2lem2  19077  nmoleub3  19080  ipcnlem2  19151  cmetcaulem  19194  cncmet  19228  minveclem4  19286  ovoliunlem1  19351  ovoliun2  19355  ovolscalem1  19362  ovolicopnf  19373  voliunlem2  19398  volsup  19403  ioorcl2  19417  uniiccvol  19425  uniioombllem4  19431  i1fd  19526  mbfi1fseqlem4  19563  itg2const2  19586  itg2eqa  19590  itg2split  19594  itg2i1fseqle  19599  itg2cnlem2  19607  dvcnv  19814  dveflem  19816  dvferm1lem  19821  dvlip2  19832  c1liplem1  19833  dvivthlem1  19845  lhop1lem  19850  dvcvx  19857  dvfsumle  19858  dvfsumabs  19860  dvfsumlem4  19866  dvfsumrlim2  19869  ftc1a  19874  deg1pwle  19995  fta1blem  20044  aalioulem3  20204  aaliou2b  20211  ulmbdd  20267  ulmdvlem1  20269  itgulm  20277  pserdvlem2  20297  abelthlem3  20302  abelthlem5  20304  abelthlem6  20305  abelthlem7  20307  tanregt0  20394  argimlt0  20461  logdivlti  20468  logcnlem3  20488  logcnlem4  20489  logtayl  20504  logtayl2  20506  cxple2  20541  cxpcn3lem  20584  cxpaddle  20589  isosctrlem1  20615  atantayl  20730  efrlim  20761  dfef2  20762  o1cxp  20766  cxp2lim  20768  divsqrsumo1  20775  amgmlem  20781  logdifbnd  20785  emcllem7  20793  harmonicbnd4  20802  fsumharmonic  20803  ftalem2  20809  basellem2  20817  basellem5  20820  basellem9  20824  vma1  20902  sqff1o  20918  fsumfldivdiaglem  20927  chtub  20949  fsumvma2  20951  chpchtsum  20956  chpub  20957  logfaclbnd  20959  logfacbnd3  20960  logfacrlim  20961  logexprlim  20962  bcmono  21014  bposlem2  21022  bposlem5  21025  bposlem6  21026  lgsne0  21070  lgsquadlem1  21091  lgsquadlem2  21092  2sqblem  21114  chebbnd1lem1  21116  chtppilimlem1  21120  chtppilimlem2  21121  chpchtlim  21126  rplogsumlem1  21131  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0re  21160  dchrisum0lem2a  21164  dchrisum0lem3  21166  dirith  21176  mulog2sumlem1  21181  mulog2sumlem2  21182  log2sumbnd  21191  selberglem2  21193  logdivbnd  21203  selberg3lem1  21204  selberg4lem1  21207  pntrsumbnd2  21214  pntrlog2bndlem1  21224  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem3  21239  pntlemb  21244  pntlemn  21247  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemo  21254  ostth2lem3  21282  ostth3  21285  nvabs  22115  nvlmle  22141  smcnlem  22146  ubthlem2  22326  minvecolem4  22335  htthlem  22373  normpyc  22601  nmophmi  23487  hstle  23686  hstles  23687  stlei  23696  xrge0npcan  24169  esumpinfval  24416  esumpinfsum  24420  esumpcvgval  24421  dya2icoseg  24580  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamucov  24775  lgamcvg2  24792  gamcvg2  24797  rescon  24886  sinccvglem  25062  circum  25064  prodmolem2a  25213  btwnxfr  25894  supaddc  26137  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem3  26157  nn0prpwlem  26215  csbrn  26346  trirn  26347  isbnd3  26383  cntotbnd  26395  bfp  26423  rrndstprj2  26430  irrapxlem1  26775  irrapxlem4  26778  pell1qrgaplem  26826  pellfundglb  26838  rmspecfund  26862  monotoddzzfi  26895  rmynn  26911  jm2.24nn  26914  jm2.17c  26917  jm2.24  26918  acongeq  26938  jm2.20nn  26958  jm2.26lem3  26962  jm2.27a  26966  jm2.27c  26968  rmydioph  26975  jm3.1lem2  26979  frlmpwfi  27130  f1linds  27163  hashgcdlem  27384  hashgcdeq  27385  cncmpmax  27570  fmul01lt1lem2  27582  clim1fr1  27594  stoweidlem1  27617  stoweidlem11  27627  stoweidlem14  27630  stoweidlem24  27640  stoweidlem26  27642  wallispilem4  27684  wallispilem5  27685  stirlinglem1  27690  1cvrjat  29957  3atlem1  29965  3atlem6  29970  llnmlplnN  30021  2llnjaN  30048  2lplnja  30101  dalem57  30211  dalawlem11  30363  dalawlem12  30364  lhp2lt  30483  lhpj1  30504  lhpm0atN  30511  4atexlemex2  30553  lautm  30576  cdleme17b  30769  cdleme20j  30800  cdleme30a  30860  cdlemg4c  31094  cdlemg17a  31143  cdlemg31c  31181  trljco  31222  cdlemk46  31430  dia2dimlem2  31548  cdlemm10N  31601  cdlemn10  31689  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem15N  31804  mapdat  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator