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

Theorem eqbrtrrd 4879
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1 (𝜑𝐴 = 𝐵)
eqbrtrrd.2 (𝜑𝐴𝑅𝐶)
Assertion
Ref Expression
eqbrtrrd (𝜑𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2823 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 4877 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856
This theorem is referenced by:  dftpos4  7615  fodomfi  8487  resfifsupp  8551  cnfcom2lem  8854  infcda1  9309  enfin1ai  9500  fin56  9509  pwcfsdom  9699  fpwwe2lem7  9752  fpwwe2  9759  canthp1lem1  9768  1nqenq  10078  prlem936  10163  lemulge11  11179  supaddc  11284  supmul1  11286  mul2lt0llt0  12167  mul2lt0lgt0  12168  xaddge0  12325  xadddi2  12364  ltexp2a  13154  leexp2a  13158  nnlesq  13210  digit1  13240  faclbnd4lem1  13319  faclbnd6  13325  facavg  13327  prsshashgt1  13434  nehash2  13492  abs3dif  14313  abs2dif  14314  limsupgre  14454  rlimclim1  14518  rlimuni  14523  rlimres2  14534  rlimcn1  14561  rlimcn1b  14562  recn2  14573  imcn2  14574  rlimo1  14589  o1rlimmul  14591  iserex  14629  isercoll  14640  caucvgrlem2  14647  caucvgr  14648  iseraltlem3  14656  summolem2a  14688  fsumge1  14770  o1fsum  14786  isumrpcl  14816  climcnds  14824  harmonic  14832  mertenslem1  14856  prodmolem2a  14904  ege2le3  15059  efgt1p2  15083  efgt1p  15084  eirrlem  15171  rpnnen2lem11  15192  fsumdvds  15272  bitsfzo  15395  bitsmod  15396  bitscmp  15398  mulgcd  15503  dvdssqlem  15517  nn0seqcvgd  15521  mulgcddvds  15606  rpdvds  15611  qden1elz  15701  phimullem  15720  hashgcdlem  15729  hashgcdeq  15730  pcdvdstr  15816  pockthg  15846  prmreclem1  15856  4sqlem11  15895  ramub1lem1  15966  ramub1lem2  15967  mreexexlem4d  16531  sscid  16707  latmlej21  17316  latmlej22  17317  lubel  17346  efginvrel1  18361  odadd2  18472  odadd  18473  gexexlem  18475  cyggex2  18518  ablfacrplem  18685  ablfac1c  18691  ablfac1eu  18693  pgpfac1lem3a  18696  isabvd  19043  mptscmfsuppd  19152  znrrg  20140  frlmphl  20350  frlmup1  20367  f1linds  20394  chcoeffeqlem  20923  lmcn2  21686  metrtri  22395  imasdsf1olem  22411  stdbdxmet  22553  nrmmetd  22612  nmmtri  22659  nlmvscnlem2  22722  blcvx  22834  recld2  22850  zdis  22852  opnreen  22867  cnheibor  22987  lebnumlem3  22995  nmoleub2lem3  23147  nmoleub2lem2  23148  nmoleub3  23151  ipcnlem2  23275  cmetcaulem  23319  nglmle  23333  cncmet  23352  csbren  23416  trirn  23417  minveclem4  23437  ovoliunlem1  23505  ovoliun2  23509  ovolscalem1  23516  ovolicopnf  23527  voliunlem2  23554  volsup  23559  ioorcl2  23575  uniiccvol  23583  uniioombllem4  23589  i1fd  23684  mbfi1fseqlem4  23721  itg2const2  23744  itg2eqa  23748  itg2split  23752  itg2i1fseqle  23757  itg2cnlem2  23765  dvcnv  23976  dveflem  23978  dvferm1lem  23983  dvlip2  23994  c1liplem1  23995  dvivthlem1  24007  lhop1lem  24012  dvcvx  24019  dvfsumle  24020  dvfsumabs  24022  dvfsumlem4  24028  dvfsumrlim2  24031  ftc1a  24036  tdeglem4  24056  deg1pwle  24115  fta1blem  24164  aalioulem3  24325  aaliou2b  24332  ulmbdd  24388  ulmdvlem1  24390  itgulm  24398  pserdvlem2  24418  abelthlem3  24423  abelthlem5  24425  abelthlem6  24426  abelthlem7  24428  tanregt0  24522  argimlt0  24595  logdivlti  24602  logcnlem3  24626  logcnlem4  24627  logtayl  24642  logtayl2  24644  cxple2  24679  cxpcn3lem  24724  cxpaddle  24729  isosctrlem1  24784  atantayl  24900  efrlim  24932  dfef2  24933  o1cxp  24937  cxp2lim  24939  divsqrtsumo1  24946  amgmlem  24952  logdifbnd  24956  emcllem7  24964  harmonicbnd4  24973  fsumharmonic  24974  lgamgulmlem2  24992  lgamgulmlem3  24993  lgamucov  25000  lgamcvg2  25017  gamcvg2  25022  ftalem2  25036  basellem2  25044  basellem5  25047  basellem9  25051  vma1  25128  sqff1o  25144  fsumfldivdiaglem  25151  chtub  25173  fsumvma2  25175  chpchtsum  25180  chpub  25181  logfaclbnd  25183  logfacbnd3  25184  logfacrlim  25185  logexprlim  25186  bcmono  25238  bposlem2  25246  bposlem5  25249  bposlem6  25250  lgsne0  25296  lgsquadlem1  25341  lgsquadlem2  25342  2sqblem  25392  chebbnd1lem1  25394  chtppilimlem1  25398  chtppilimlem2  25399  chpchtlim  25404  rplogsumlem1  25409  dchrvmasumiflem1  25426  dchrisum0flblem2  25434  dchrisum0fno1  25436  dchrisum0re  25438  dchrisum0lem2a  25442  dchrisum0lem3  25444  dirith  25454  mulog2sumlem1  25459  mulog2sumlem2  25460  log2sumbnd  25469  selberglem2  25471  logdivbnd  25481  selberg3lem1  25482  selberg4lem1  25485  pntrsumbnd2  25492  pntrlog2bndlem1  25502  pntrlog2bndlem5  25506  pntrlog2bndlem6  25508  pntpbnd1a  25510  pntpbnd1  25511  pntpbnd2  25512  pntibndlem3  25517  pntlemb  25522  pntlemn  25525  pntlemr  25527  pntlemj  25528  pntlemf  25530  pntlemo  25532  ostth2lem3  25560  ostth3  25563  footeq  25852  hlperpnel  25853  perpdragALT  25855  perpdrag  25856  colperp  25857  mideulem2  25862  opphllem  25863  opphllem3  25877  lmieu  25912  trgcopy  25932  sacgr  25958  acopyeu  25961  usgredgleordALT  26364  eucrctshift  27438  nvabs  27877  smcnlem  27902  ubthlem2  28077  minvecolem4  28086  htthlem  28124  normpyc  28353  nmophmi  29240  hstle  29439  hstles  29440  stlei  29449  nnmulge  29864  fsumiunle  29924  2sqmod  29995  xrge0npcan  30041  archirngz  30090  archiabllem1a  30092  archiabllem2a  30095  archiabllem2c  30096  ornglmulle  30152  orngrmulle  30153  madjusmdetlem2  30241  esumpinfval  30482  esumpinfsum  30486  esumpcvgval  30487  esum2d  30502  esumiun  30503  dya2icoseg  30686  omssubadd  30709  carsgsigalem  30724  carsggect  30727  carsgclctunlem3  30729  omsmeas  30732  eulerpartlems  30769  sgnmulsgn  30958  signsplypnf  30974  signsply0  30975  reprlt  31044  reprinfz1  31047  hgt750lemc  31072  hgt750lemf  31078  resconn  31572  sinccvglem  31909  circum  31911  btwnxfr  32505  nn0prpwlem  32659  dnibndlem2  32807  poimirlem7  33747  mblfinlem3  33779  mblfinlem4  33780  itg2addnclem3  33793  ftc1anc  33823  isbnd3  33912  cntotbnd  33924  bfp  33952  rrndstprj2  33959  1cvrjat  35273  3atlem1  35281  3atlem6  35286  llnmlplnN  35337  2llnjaN  35364  2lplnja  35417  dalem57  35527  dalawlem11  35679  dalawlem12  35680  lhp2lt  35799  lhpj1  35820  lhpm0atN  35827  4atexlemex2  35869  lautm  35892  cdleme17b  36085  cdleme20j  36116  cdleme30a  36176  cdlemg4c  36410  cdlemg17a  36459  cdlemg31c  36497  trljco  36538  cdlemk46  36746  dia2dimlem2  36863  cdlemm10N  36916  cdlemn10  37004  dihmeetlem1N  37088  dihglblem5apreN  37089  dihmeetlem15N  37119  mapdat  37465  irrapxlem1  37905  irrapxlem4  37908  pell1qrgaplem  37956  pellfundglb  37968  rmspecfund  37992  monotoddzzfi  38025  rmynn  38041  jm2.24nn  38044  jm2.17c  38047  jm2.24  38048  acongeq  38068  jm2.20nn  38082  jm2.26lem3  38086  jm2.27a  38090  jm2.27c  38092  rmydioph  38099  jm3.1lem2  38103  frlmpwfi  38186  areaquad  38319  rp-isfinite6  38381  frege129d  38572  leeq1d  38972  imo72b2  38992  cvgdvgrat  39029  radcnvrat  39030  hashnzfzclim  39038  isosctrlem1ALT  39681  cncmpmax  39702  iooabslt  40222  fmul01lt1lem2  40314  clim1fr1  40330  limcrecl  40358  climxrrelem  40478  stoweidlem1  40714  stoweidlem11  40724  stoweidlem14  40727  stoweidlem24  40737  stoweidlem26  40739  wallispilem4  40781  wallispilem5  40782  stirlinglem1  40787  fourierdlem51  40870  fourierdlem65  40884  fouriersw  40944  2leaddle2  41905  sqrtpwpw2p  42042  lighneallem4a  42117  flnn0div2ge  42912  logbpw2m1  42946  amgmwlem  43136
  Copyright terms: Public domain W3C validator