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

Theorem eqbrtrrd 4709
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 2657 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 4707 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  dftpos4  7416  fodomfi  8280  resfifsupp  8344  cnfcom2lem  8636  infcda1  9053  enfin1ai  9244  fin56  9253  pwcfsdom  9443  fpwwe2lem7  9496  fpwwe2  9503  canthp1lem1  9512  1nqenq  9822  prlem936  9907  lemulge11  10923  supaddc  11028  supmul1  11030  mul2lt0llt0  11972  mul2lt0lgt0  11973  xaddge0  12126  xadddi2  12165  ltexp2a  12952  leexp2a  12956  nnlesq  13008  digit1  13038  faclbnd4lem1  13120  faclbnd6  13126  facavg  13128  prsshashgt1  13236  nehash2  13294  abs3dif  14115  abs2dif  14116  limsupgre  14256  rlimclim1  14320  rlimuni  14325  rlimres2  14336  rlimcn1  14363  rlimcn1b  14364  recn2  14375  imcn2  14376  rlimo1  14391  o1rlimmul  14393  iserex  14431  isercoll  14442  caucvgrlem2  14449  caucvgr  14450  iseraltlem3  14458  summolem2a  14490  fsumge1  14573  o1fsum  14589  isumrpcl  14619  climcnds  14627  harmonic  14635  mertenslem1  14660  prodmolem2a  14708  ege2le3  14864  efgt1p2  14888  efgt1p  14889  eirrlem  14976  rpnnen2lem11  14997  fsumdvds  15077  bitsfzo  15204  bitsmod  15205  bitscmp  15207  mulgcd  15312  dvdssqlem  15326  nn0seqcvgd  15330  mulgcddvds  15416  rpdvds  15421  qden1elz  15512  phimullem  15531  hashgcdlem  15540  hashgcdeq  15541  pcdvdstr  15627  pockthg  15657  prmreclem1  15667  4sqlem11  15706  ramub1lem1  15777  ramub1lem2  15778  mreexexlem4d  16354  sscid  16531  latmlej21  17139  latmlej22  17140  lubel  17169  efginvrel1  18187  odadd2  18298  odadd  18299  gexexlem  18301  cyggex2  18344  ablfacrplem  18510  ablfac1c  18516  ablfac1eu  18518  pgpfac1lem3a  18521  isabvd  18868  mptscmfsuppd  18977  znrrg  19962  frlmphl  20168  frlmup1  20185  f1linds  20212  chcoeffeqlem  20738  lmcn2  21500  metrtri  22209  imasdsf1olem  22225  stdbdxmet  22367  nrmmetd  22426  nmmtri  22473  nlmvscnlem2  22536  blcvx  22648  recld2  22664  zdis  22666  opnreen  22681  cnheibor  22801  lebnumlem3  22809  nmoleub2lem3  22961  nmoleub2lem2  22962  nmoleub3  22965  ipcnlem2  23089  cmetcaulem  23132  nglmle  23146  cncmet  23165  csbren  23228  trirn  23229  minveclem4  23249  ovoliunlem1  23316  ovoliun2  23320  ovolscalem1  23327  ovolicopnf  23338  voliunlem2  23365  volsup  23370  ioorcl2  23386  uniiccvol  23394  uniioombllem4  23400  i1fd  23493  mbfi1fseqlem4  23530  itg2const2  23553  itg2eqa  23557  itg2split  23561  itg2i1fseqle  23566  itg2cnlem2  23574  dvcnv  23785  dveflem  23787  dvferm1lem  23792  dvlip2  23803  c1liplem1  23804  dvivthlem1  23816  lhop1lem  23821  dvcvx  23828  dvfsumle  23829  dvfsumabs  23831  dvfsumlem4  23837  dvfsumrlim2  23840  ftc1a  23845  tdeglem4  23865  deg1pwle  23924  fta1blem  23973  aalioulem3  24134  aaliou2b  24141  ulmbdd  24197  ulmdvlem1  24199  itgulm  24207  pserdvlem2  24227  abelthlem3  24232  abelthlem5  24234  abelthlem6  24235  abelthlem7  24237  tanregt0  24330  argimlt0  24404  logdivlti  24411  logcnlem3  24435  logcnlem4  24436  logtayl  24451  logtayl2  24453  cxple2  24488  cxpcn3lem  24533  cxpaddle  24538  isosctrlem1  24593  atantayl  24709  efrlim  24741  dfef2  24742  o1cxp  24746  cxp2lim  24748  divsqrtsumo1  24755  amgmlem  24761  logdifbnd  24765  emcllem7  24773  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamucov  24809  lgamcvg2  24826  gamcvg2  24831  ftalem2  24845  basellem2  24853  basellem5  24856  basellem9  24860  vma1  24937  sqff1o  24953  fsumfldivdiaglem  24960  chtub  24982  fsumvma2  24984  chpchtsum  24989  chpub  24990  logfaclbnd  24992  logfacbnd3  24993  logfacrlim  24994  logexprlim  24995  bcmono  25047  bposlem2  25055  bposlem5  25058  bposlem6  25059  lgsne0  25105  lgsquadlem1  25150  lgsquadlem2  25151  2sqblem  25201  chebbnd1lem1  25203  chtppilimlem1  25207  chtppilimlem2  25208  chpchtlim  25213  rplogsumlem1  25218  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  dchrisum0lem2a  25251  dchrisum0lem3  25253  dirith  25263  mulog2sumlem1  25268  mulog2sumlem2  25269  log2sumbnd  25278  selberglem2  25280  logdivbnd  25290  selberg3lem1  25291  selberg4lem1  25294  pntrsumbnd2  25301  pntrlog2bndlem1  25311  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem3  25326  pntlemb  25331  pntlemn  25334  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemo  25341  ostth2lem3  25369  ostth3  25372  footeq  25661  hlperpnel  25662  perpdragALT  25664  perpdrag  25665  colperp  25666  mideulem2  25671  opphllem  25672  opphllem3  25686  lmieu  25721  trgcopy  25741  sacgr  25767  acopyeu  25770  usgredgleordALT  26171  eucrctshift  27221  nvabs  27655  smcnlem  27680  ubthlem2  27855  minvecolem4  27864  htthlem  27902  normpyc  28131  nmophmi  29018  hstle  29217  hstles  29218  stlei  29227  nnmulge  29643  fsumiunle  29703  2sqmod  29776  xrge0npcan  29822  archirngz  29871  archiabllem1a  29873  archiabllem2a  29876  archiabllem2c  29877  ornglmulle  29933  orngrmulle  29934  madjusmdetlem2  30022  esumpinfval  30263  esumpinfsum  30267  esumpcvgval  30268  esum2d  30283  esumiun  30284  dya2icoseg  30467  omssubadd  30490  carsgsigalem  30505  carsggect  30508  carsgclctunlem3  30510  omsmeas  30513  eulerpartlems  30550  sgnmulsgn  30739  signsplypnf  30755  signsply0  30756  reprlt  30825  reprinfz1  30828  hgt750lemc  30853  hgt750lemf  30859  resconn  31354  sinccvglem  31692  circum  31694  btwnxfr  32288  nn0prpwlem  32442  dnibndlem2  32594  poimirlem7  33546  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem3  33593  ftc1anc  33623  isbnd3  33713  cntotbnd  33725  bfp  33753  rrndstprj2  33760  1cvrjat  35079  3atlem1  35087  3atlem6  35092  llnmlplnN  35143  2llnjaN  35170  2lplnja  35223  dalem57  35333  dalawlem11  35485  dalawlem12  35486  lhp2lt  35605  lhpj1  35626  lhpm0atN  35633  4atexlemex2  35675  lautm  35698  cdleme17b  35892  cdleme20j  35923  cdleme30a  35983  cdlemg4c  36217  cdlemg17a  36266  cdlemg31c  36304  trljco  36345  cdlemk46  36553  dia2dimlem2  36671  cdlemm10N  36724  cdlemn10  36812  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem15N  36927  mapdat  37273  irrapxlem1  37703  irrapxlem4  37706  pell1qrgaplem  37754  pellfundglb  37766  rmspecfund  37791  monotoddzzfi  37824  rmynn  37840  jm2.24nn  37843  jm2.17c  37846  jm2.24  37847  acongeq  37867  jm2.20nn  37881  jm2.26lem3  37885  jm2.27a  37889  jm2.27c  37891  rmydioph  37898  jm3.1lem2  37902  frlmpwfi  37985  areaquad  38119  rp-isfinite6  38181  frege129d  38372  leeq1d  38772  imo72b2  38792  cvgdvgrat  38829  radcnvrat  38830  hashnzfzclim  38838  isosctrlem1ALT  39484  cncmpmax  39505  iooabslt  40039  fmul01lt1lem2  40135  clim1fr1  40151  limcrecl  40179  climxrrelem  40299  stoweidlem1  40536  stoweidlem11  40546  stoweidlem14  40549  stoweidlem24  40559  stoweidlem26  40561  wallispilem4  40603  wallispilem5  40604  stirlinglem1  40609  fourierdlem51  40692  fourierdlem65  40706  fouriersw  40766  2leaddle2  41637  sqrtpwpw2p  41775  lighneallem4a  41850  flnn0div2ge  42652  logbpw2m1  42686  amgmwlem  42876
  Copyright terms: Public domain W3C validator