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

Theorem eqbrtrrd 4601
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 2615 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 4599 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  dftpos4  7235  fodomfi  8101  resfifsupp  8163  cnfcom2lem  8458  infcda1  8875  enfin1ai  9066  fin56  9075  pwcfsdom  9261  fpwwe2lem7  9314  fpwwe2  9321  canthp1lem1  9330  1nqenq  9640  prlem936  9725  lemulge11  10734  supaddc  10837  supmul1  10839  mul2lt0llt0  11766  mul2lt0lgt0  11767  xaddge0  11917  xadddi2  11956  ltexp2a  12729  leexp2a  12733  nnlesq  12785  digit1  12815  faclbnd4lem1  12897  faclbnd6  12903  facavg  12905  prsshashgt1  13011  abs3dif  13865  abs2dif  13866  limsupgre  14006  rlimclim1  14070  rlimuni  14075  rlimres2  14086  rlimcn1  14113  rlimcn1b  14114  recn2  14125  imcn2  14126  rlimo1  14141  o1rlimmul  14143  iserex  14181  isercoll  14192  caucvgrlem2  14199  caucvgr  14200  iseraltlem3  14208  summolem2a  14239  fsumge1  14316  o1fsum  14332  isumrpcl  14360  climcnds  14368  harmonic  14376  mertenslem1  14401  prodmolem2a  14449  ege2le3  14605  efgt1p2  14629  efgt1p  14630  eirrlem  14717  rpnnen2lem11  14738  fsumdvds  14814  bitsfzo  14941  bitsmod  14942  bitscmp  14944  mulgcd  15049  dvdssqlem  15063  nn0seqcvgd  15067  mulgcddvds  15153  rpdvds  15158  qden1elz  15249  phimullem  15268  hashgcdlem  15277  hashgcdeq  15278  pcdvdstr  15364  pockthg  15394  prmreclem1  15404  4sqlem11  15443  ramub1lem1  15514  ramub1lem2  15515  mreexexlem4d  16076  sscid  16253  latmlej21  16861  latmlej22  16862  lubel  16891  efginvrel1  17910  odadd2  18021  odadd  18022  gexexlem  18024  cyggex2  18067  ablfacrplem  18233  ablfac1c  18239  ablfac1eu  18241  pgpfac1lem3a  18244  isabvd  18589  mptscmfsuppd  18698  znrrg  19678  frlmphl  19881  frlmup1  19898  f1linds  19925  chcoeffeqlem  20451  lmcn2  21204  metrtri  21913  imasdsf1olem  21929  stdbdxmet  22071  nrmmetd  22130  nmmtri  22176  nlmvscnlem2  22232  blcvx  22341  recld2  22357  zdis  22359  opnreen  22374  cnheibor  22493  lebnumlem3  22501  nmoleub2lem3  22654  nmoleub2lem2  22655  nmoleub3  22658  ipcnlem2  22769  cmetcaulem  22812  cncmet  22844  csbren  22907  trirn  22908  minveclem4  22928  ovoliunlem1  22994  ovoliun2  22998  ovolscalem1  23005  ovolicopnf  23016  voliunlem2  23043  volsup  23048  ioorcl2  23063  uniiccvol  23071  uniioombllem4  23077  i1fd  23171  mbfi1fseqlem4  23208  itg2const2  23231  itg2eqa  23235  itg2split  23239  itg2i1fseqle  23244  itg2cnlem2  23252  dvcnv  23461  dveflem  23463  dvferm1lem  23468  dvlip2  23479  c1liplem1  23480  dvivthlem1  23492  lhop1lem  23497  dvcvx  23504  dvfsumle  23505  dvfsumabs  23507  dvfsumlem4  23513  dvfsumrlim2  23516  ftc1a  23521  tdeglem4  23541  deg1pwle  23600  fta1blem  23649  aalioulem3  23810  aaliou2b  23817  ulmbdd  23873  ulmdvlem1  23875  itgulm  23883  pserdvlem2  23903  abelthlem3  23908  abelthlem5  23910  abelthlem6  23911  abelthlem7  23913  tanregt0  24006  argimlt0  24080  logdivlti  24087  logcnlem3  24107  logcnlem4  24108  logtayl  24123  logtayl2  24125  cxple2  24160  cxpcn3lem  24205  cxpaddle  24210  isosctrlem1  24265  atantayl  24381  efrlim  24413  dfef2  24414  o1cxp  24418  cxp2lim  24420  divsqrtsumo1  24427  amgmlem  24433  logdifbnd  24437  emcllem7  24445  harmonicbnd4  24454  fsumharmonic  24455  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamucov  24481  lgamcvg2  24498  gamcvg2  24503  ftalem2  24517  basellem2  24525  basellem5  24528  basellem9  24532  vma1  24609  sqff1o  24625  fsumfldivdiaglem  24632  chtub  24654  fsumvma2  24656  chpchtsum  24661  chpub  24662  logfaclbnd  24664  logfacbnd3  24665  logfacrlim  24666  logexprlim  24667  bcmono  24719  bposlem2  24727  bposlem5  24730  bposlem6  24731  lgsne0  24777  lgsquadlem1  24822  lgsquadlem2  24823  2sqblem  24873  chebbnd1lem1  24875  chtppilimlem1  24879  chtppilimlem2  24880  chpchtlim  24885  rplogsumlem1  24890  dchrvmasumiflem1  24907  dchrisum0flblem2  24915  dchrisum0fno1  24917  dchrisum0re  24919  dchrisum0lem2a  24923  dchrisum0lem3  24925  dirith  24935  mulog2sumlem1  24940  mulog2sumlem2  24941  log2sumbnd  24950  selberglem2  24952  logdivbnd  24962  selberg3lem1  24963  selberg4lem1  24966  pntrsumbnd2  24973  pntrlog2bndlem1  24983  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem3  24998  pntlemb  25003  pntlemn  25006  pntlemr  25008  pntlemj  25009  pntlemf  25011  pntlemo  25013  ostth2lem3  25041  ostth3  25044  nehash2  25120  footeq  25334  hlperpnel  25335  perpdragALT  25337  perpdrag  25338  colperp  25339  mideulem2  25344  opphllem  25345  opphllem3  25359  lmieu  25394  trgcopy  25414  sacgr  25440  acopyeu  25443  nvabs  26706  nvlmle  26732  smcnlem  26737  ubthlem2  26917  minvecolem4  26926  htthlem  26964  normpyc  27193  nmophmi  28080  hstle  28279  hstles  28280  stlei  28289  2sqmod  28785  xrge0npcan  28831  archirngz  28880  archiabllem1a  28882  archiabllem2a  28885  archiabllem2c  28886  ornglmulle  28942  orngrmulle  28943  madjusmdetlem2  29028  esumpinfval  29268  esumpinfsum  29272  esumpcvgval  29273  esum2d  29288  esumiun  29289  dya2icoseg  29472  omssubadd  29495  carsgsigalem  29510  carsggect  29513  carsgclctunlem3  29515  omsmeas  29518  eulerpartlems  29555  sgnmulsgn  29744  signsplypnf  29759  signsply0  29760  rescon  30288  sinccvglem  30626  circum  30628  btwnxfr  31139  nn0prpwlem  31293  dnibndlem2  31445  poimirlem7  32382  mblfinlem3  32414  mblfinlem4  32415  itg2addnclem3  32429  ftc1anc  32459  isbnd3  32549  cntotbnd  32561  bfp  32589  rrndstprj2  32596  1cvrjat  33575  3atlem1  33583  3atlem6  33588  llnmlplnN  33639  2llnjaN  33666  2lplnja  33719  dalem57  33829  dalawlem11  33981  dalawlem12  33982  lhp2lt  34101  lhpj1  34122  lhpm0atN  34129  4atexlemex2  34171  lautm  34194  cdleme17b  34388  cdleme20j  34420  cdleme30a  34480  cdlemg4c  34714  cdlemg17a  34763  cdlemg31c  34801  trljco  34842  cdlemk46  35050  dia2dimlem2  35168  cdlemm10N  35221  cdlemn10  35309  dihmeetlem1N  35393  dihglblem5apreN  35394  dihmeetlem15N  35424  mapdat  35770  irrapxlem1  36200  irrapxlem4  36203  pell1qrgaplem  36251  pellfundglb  36263  rmspecfund  36288  monotoddzzfi  36321  rmynn  36337  jm2.24nn  36340  jm2.17c  36343  jm2.24  36344  acongeq  36364  jm2.20nn  36378  jm2.26lem3  36382  jm2.27a  36386  jm2.27c  36388  rmydioph  36395  jm3.1lem2  36399  frlmpwfi  36482  areaquad  36617  rp-isfinite6  36679  frege129d  36870  imo72b2  37293  cvgdvgrat  37330  radcnvrat  37331  hashnzfzclim  37339  isosctrlem1ALT  37988  cncmpmax  38010  iooabslt  38365  fmul01lt1lem2  38449  clim1fr1  38465  limcrecl  38493  stoweidlem1  38691  stoweidlem11  38701  stoweidlem14  38704  stoweidlem24  38714  stoweidlem26  38716  wallispilem4  38758  wallispilem5  38759  stirlinglem1  38764  fourierdlem51  38847  fourierdlem65  38861  fouriersw  38921  sqrtpwpw2p  39786  lighneallem4a  39861  2leaddle2  40164  usgredgaleordALT  40456  eucrctshift  41406  flnn0div2ge  42116  logbpw2m1  42154  amgmwlem  42313
  Copyright terms: Public domain W3C validator