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

Theorem eqbrtrrd 5077
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 2830 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 5075 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538   class class class wbr 5053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3483  df-un 3925  df-sn 4552  df-pr 4554  df-op 4558  df-br 5054
This theorem is referenced by:  dftpos4  7908  fodomfi  8795  resfifsupp  8859  cnfcom2lem  9162  enfin1ai  9805  pwcfsdom  10004  fpwwe2lem7  10057  fpwwe2  10064  canthp1lem1  10073  1nqenq  10383  prlem936  10468  lemulge11  11501  supaddc  11607  supmul1  11609  mul2lt0llt0  12493  mul2lt0lgt0  12494  xaddge0  12651  xadddi2  12690  ltexp2a  13538  leexp2a  13544  nnlesq  13576  digit1  13606  faclbnd4lem1  13661  faclbnd6  13667  facavg  13669  prsshashgt1  13779  nehash2  13840  abs3dif  14694  abs2dif  14695  limsupgre  14841  rlimclim1  14905  rlimuni  14910  rlimres2  14921  rlimcn1  14948  rlimcn1b  14949  recn2  14960  imcn2  14961  rlimo1  14976  o1rlimmul  14978  iserex  15016  isercoll  15027  caucvgrlem2  15034  caucvgr  15035  iseraltlem3  15043  summolem2a  15075  fsumge1  15155  o1fsum  15171  isumrpcl  15201  climcnds  15209  harmonic  15217  mertenslem1  15243  prodmolem2a  15291  ege2le3  15446  efgt1p2  15470  efgt1p  15471  eirrlem  15560  rpnnen2lem11  15580  fsumdvds  15661  bitsfzo  15785  bitsmod  15786  bitscmp  15788  mulgcd  15897  dvdssqlem  15911  nn0seqcvgd  15915  mulgcddvds  16000  rpdvds  16005  qden1elz  16098  phimullem  16117  hashgcdlem  16126  hashgcdeq  16127  pcdvdstr  16213  pockthg  16243  prmreclem1  16253  4sqlem11  16292  ramub1lem1  16363  ramub1lem2  16364  mreexexlem4d  16921  sscid  17097  latmlej21  17705  latmlej22  17706  lubel  17735  efginvrel1  18857  odadd2  18972  odadd  18973  gexexlem  18975  cyggex2  19020  ablfacrplem  19190  ablfac1c  19196  ablfac1eu  19198  pgpfac1lem3a  19201  isabvd  19594  mptscmfsuppd  19703  znrrg  20715  frlmphl  20928  frlmup1  20945  f1linds  20972  chcoeffeqlem  21496  lmcn2  22260  metrtri  22970  imasdsf1olem  22986  stdbdxmet  23128  nrmmetd  23187  nmmtri  23234  nlmvscnlem2  23297  blcvx  23409  recld2  23425  zdis  23427  opnreen  23442  cnheibor  23566  lebnumlem3  23574  nmoleub2lem3  23726  nmoleub2lem2  23727  nmoleub3  23730  ipcnlem2  23854  cmetcaulem  23898  nglmle  23912  cncmet  23932  csbren  24009  trirn  24010  minveclem4  24042  ovoliunlem1  24112  ovoliun2  24116  ovolscalem1  24123  ovolicopnf  24134  voliunlem2  24161  volsup  24166  ioorcl2  24182  uniiccvol  24190  uniioombllem4  24196  i1fd  24291  mbfi1fseqlem4  24328  itg2const2  24351  itg2eqa  24355  itg2split  24359  itg2i1fseqle  24364  itg2cnlem2  24372  dvcnv  24586  dveflem  24588  dvferm1lem  24593  dvlip2  24604  c1liplem1  24605  dvivthlem1  24617  lhop1lem  24622  dvcvx  24629  dvfsumle  24630  dvfsumabs  24632  dvfsumlem4  24638  dvfsumrlim2  24641  ftc1a  24646  tdeglem4  24667  deg1pwle  24726  fta1blem  24775  aalioulem3  24936  aaliou2b  24943  ulmbdd  24999  ulmdvlem1  25001  itgulm  25009  pserdvlem2  25029  abelthlem3  25034  abelthlem5  25036  abelthlem6  25037  abelthlem7  25039  tanregt0  25137  argimlt0  25210  logdivlti  25217  logcnlem3  25241  logcnlem4  25242  logtayl  25257  logtayl2  25259  cxple2  25294  cxpcn3lem  25342  cxpaddle  25347  isosctrlem1  25410  atantayl  25529  efrlim  25561  dfef2  25562  o1cxp  25566  cxp2lim  25568  divsqrtsumo1  25575  amgmlem  25581  logdifbnd  25585  emcllem7  25593  harmonicbnd4  25602  fsumharmonic  25603  lgamgulmlem2  25621  lgamgulmlem3  25622  lgamucov  25629  lgamcvg2  25646  gamcvg2  25651  ftalem2  25665  basellem2  25673  basellem5  25676  basellem9  25680  vma1  25757  sqff1o  25773  fsumfldivdiaglem  25780  chtub  25802  fsumvma2  25804  chpchtsum  25809  chpub  25810  logfaclbnd  25812  logfacbnd3  25813  logfacrlim  25814  logexprlim  25815  bcmono  25867  bposlem2  25875  bposlem5  25878  bposlem6  25879  lgsne0  25925  lgsquadlem1  25970  lgsquadlem2  25971  2sqblem  26021  2sqmod  26026  chebbnd1lem1  26059  chtppilimlem1  26063  chtppilimlem2  26064  chpchtlim  26069  rplogsumlem1  26074  dchrvmasumiflem1  26091  dchrisum0flblem2  26099  dchrisum0fno1  26101  dchrisum0lem2a  26107  dchrisum0lem3  26109  dirith  26119  mulog2sumlem1  26124  mulog2sumlem2  26125  log2sumbnd  26134  selberglem2  26136  logdivbnd  26146  selberg3lem1  26147  selberg4lem1  26150  pntrsumbnd2  26157  pntrlog2bndlem1  26167  pntrlog2bndlem5  26171  pntrlog2bndlem6  26173  pntpbnd1a  26175  pntpbnd1  26176  pntpbnd2  26177  pntibndlem3  26182  pntlemb  26187  pntlemn  26190  pntlemr  26192  pntlemj  26193  pntlemf  26195  pntlemo  26197  ostth2lem3  26225  ostth3  26228  footeq  26524  hlperpnel  26525  perpdragALT  26527  perpdrag  26528  colperp  26529  mideulem2  26534  opphllem  26535  opphllem3  26549  lmieu  26584  trgcopy  26604  sacgr  26631  acopyeu  26634  usgredgleordALT  27030  eucrctshift  28034  nvabs  28461  smcnlem  28486  ubthlem2  28660  minvecolem4  28669  htthlem  28706  normpyc  28935  nmophmi  29820  hstle  30019  hstles  30020  stlei  30029  f1rnen  30388  fmptssfisupp  30442  nnmulge  30488  fsumiunle  30559  wrdt2ind  30641  xrge0npcan  30716  trsp2cyc  30800  archirngz  30853  archiabllem1a  30855  archiabllem2a  30858  archiabllem2c  30859  ornglmulle  30914  orngrmulle  30915  drngdimgt0  31079  lbsdiflsp0  31085  madjusmdetlem2  31156  esumpinfval  31392  esumpinfsum  31396  esumpcvgval  31397  esum2d  31412  esumiun  31413  dya2icoseg  31595  omssubadd  31618  carsgsigalem  31633  carsggect  31636  carsgclctunlem3  31638  omsmeas  31641  eulerpartlems  31678  sgnmulsgn  31867  signsplypnf  31880  signsply0  31881  reprlt  31950  reprinfz1  31953  hgt750lemc  31978  hgt750lemf  31984  pthhashvtx  32434  resconn  32553  sinccvglem  32975  circum  32977  btwnxfr  33577  nn0prpwlem  33730  dnibndlem2  33878  unblimceq0  33906  irrdiff  34688  poimirlem7  35010  mblfinlem3  35042  mblfinlem4  35043  itg2addnclem3  35056  ftc1anc  35084  isbnd3  35168  cntotbnd  35180  bfp  35208  rrndstprj2  35215  1cvrjat  36717  3atlem1  36725  3atlem6  36730  llnmlplnN  36781  2llnjaN  36808  2lplnja  36861  dalem57  36971  dalawlem11  37123  dalawlem12  37124  lhp2lt  37243  lhpj1  37264  lhpm0atN  37271  4atexlemex2  37313  lautm  37336  cdleme17b  37529  cdleme20j  37560  cdleme30a  37620  cdlemg4c  37854  cdlemg17a  37903  cdlemg31c  37941  trljco  37982  cdlemk46  38190  dia2dimlem2  38307  cdlemm10N  38360  cdlemn10  38448  dihmeetlem1N  38532  dihglblem5apreN  38533  dihmeetlem15N  38563  mapdat  38909  lcmineqlem19  39284  lcmineqlem20  39285  3lexlogpow5ineq2  39291  2xp3dxp2ge1d  39325  factwoffsmonot  39326  rtprmirr  39433  fltnlta  39536  3cubeslem1  39542  irrapxlem1  39680  irrapxlem4  39683  pell1qrgaplem  39731  pellfundglb  39743  rmspecfund  39767  monotoddzzfi  39800  rmynn  39814  jm2.24nn  39817  jm2.17c  39820  jm2.24  39821  acongeq  39841  jm2.20nn  39855  jm2.26lem3  39859  jm2.27a  39863  jm2.27c  39865  rmydioph  39872  jm3.1lem2  39876  frlmpwfi  39959  areaquad  40083  rp-isfinite6  40143  frege129d  40381  leeq1d  40780  imo72b2  40798  cvgdvgrat  40938  radcnvrat  40939  hashnzfzclim  40947  isosctrlem1ALT  41561  cncmpmax  41582  iooabslt  42063  fmul01lt1lem2  42154  clim1fr1  42170  limcrecl  42198  climxrrelem  42318  liminflbuz2  42384  stoweidlem1  42570  stoweidlem11  42580  stoweidlem14  42583  stoweidlem24  42593  stoweidlem26  42595  wallispilem4  42637  wallispilem5  42638  stirlinglem1  42643  fourierdlem51  42726  fourierdlem65  42740  fouriersw  42800  2leaddle2  43782  sqrtpwpw2p  43982  lighneallem4a  44053  flnn0div2ge  44874  logbpw2m1  44908  amgmwlem  45257
  Copyright terms: Public domain W3C validator