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

Theorem eqbrtrrd 5082
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 2827 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 5080 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  dftpos4  7902  fodomfi  8786  resfifsupp  8850  cnfcom2lem  9153  enfin1ai  9795  pwcfsdom  9994  fpwwe2lem7  10047  fpwwe2  10054  canthp1lem1  10063  1nqenq  10373  prlem936  10458  lemulge11  11491  supaddc  11597  supmul1  11599  mul2lt0llt0  12483  mul2lt0lgt0  12484  xaddge0  12641  xadddi2  12680  ltexp2a  13520  leexp2a  13526  nnlesq  13558  digit1  13588  faclbnd4lem1  13643  faclbnd6  13649  facavg  13651  prsshashgt1  13761  nehash2  13822  abs3dif  14681  abs2dif  14682  limsupgre  14828  rlimclim1  14892  rlimuni  14897  rlimres2  14908  rlimcn1  14935  rlimcn1b  14936  recn2  14947  imcn2  14948  rlimo1  14963  o1rlimmul  14965  iserex  15003  isercoll  15014  caucvgrlem2  15021  caucvgr  15022  iseraltlem3  15030  summolem2a  15062  fsumge1  15142  o1fsum  15158  isumrpcl  15188  climcnds  15196  harmonic  15204  mertenslem1  15230  prodmolem2a  15278  ege2le3  15433  efgt1p2  15457  efgt1p  15458  eirrlem  15547  rpnnen2lem11  15567  fsumdvds  15648  bitsfzo  15774  bitsmod  15775  bitscmp  15777  mulgcd  15886  dvdssqlem  15900  nn0seqcvgd  15904  mulgcddvds  15989  rpdvds  15994  qden1elz  16087  phimullem  16106  hashgcdlem  16115  hashgcdeq  16116  pcdvdstr  16202  pockthg  16232  prmreclem1  16242  4sqlem11  16281  ramub1lem1  16352  ramub1lem2  16353  mreexexlem4d  16908  sscid  17084  latmlej21  17692  latmlej22  17693  lubel  17722  efginvrel1  18785  odadd2  18900  odadd  18901  gexexlem  18903  cyggex2  18948  ablfacrplem  19118  ablfac1c  19124  ablfac1eu  19126  pgpfac1lem3a  19129  isabvd  19522  mptscmfsuppd  19631  znrrg  20642  frlmphl  20855  frlmup1  20872  f1linds  20899  chcoeffeqlem  21423  lmcn2  22187  metrtri  22896  imasdsf1olem  22912  stdbdxmet  23054  nrmmetd  23113  nmmtri  23160  nlmvscnlem2  23223  blcvx  23335  recld2  23351  zdis  23353  opnreen  23368  cnheibor  23488  lebnumlem3  23496  nmoleub2lem3  23648  nmoleub2lem2  23649  nmoleub3  23652  ipcnlem2  23776  cmetcaulem  23820  nglmle  23834  cncmet  23854  csbren  23931  trirn  23932  minveclem4  23964  ovoliunlem1  24032  ovoliun2  24036  ovolscalem1  24043  ovolicopnf  24054  voliunlem2  24081  volsup  24086  ioorcl2  24102  uniiccvol  24110  uniioombllem4  24116  i1fd  24211  mbfi1fseqlem4  24248  itg2const2  24271  itg2eqa  24275  itg2split  24279  itg2i1fseqle  24284  itg2cnlem2  24292  dvcnv  24503  dveflem  24505  dvferm1lem  24510  dvlip2  24521  c1liplem1  24522  dvivthlem1  24534  lhop1lem  24539  dvcvx  24546  dvfsumle  24547  dvfsumabs  24549  dvfsumlem4  24555  dvfsumrlim2  24558  ftc1a  24563  tdeglem4  24583  deg1pwle  24642  fta1blem  24691  aalioulem3  24852  aaliou2b  24859  ulmbdd  24915  ulmdvlem1  24917  itgulm  24925  pserdvlem2  24945  abelthlem3  24950  abelthlem5  24952  abelthlem6  24953  abelthlem7  24955  tanregt0  25050  argimlt0  25123  logdivlti  25130  logcnlem3  25154  logcnlem4  25155  logtayl  25170  logtayl2  25172  cxple2  25207  cxpcn3lem  25255  cxpaddle  25260  isosctrlem1  25323  atantayl  25442  efrlim  25475  dfef2  25476  o1cxp  25480  cxp2lim  25482  divsqrtsumo1  25489  amgmlem  25495  logdifbnd  25499  emcllem7  25507  harmonicbnd4  25516  fsumharmonic  25517  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamucov  25543  lgamcvg2  25560  gamcvg2  25565  ftalem2  25579  basellem2  25587  basellem5  25590  basellem9  25594  vma1  25671  sqff1o  25687  fsumfldivdiaglem  25694  chtub  25716  fsumvma2  25718  chpchtsum  25723  chpub  25724  logfaclbnd  25726  logfacbnd3  25727  logfacrlim  25728  logexprlim  25729  bcmono  25781  bposlem2  25789  bposlem5  25792  bposlem6  25793  lgsne0  25839  lgsquadlem1  25884  lgsquadlem2  25885  2sqblem  25935  2sqmod  25940  chebbnd1lem1  25973  chtppilimlem1  25977  chtppilimlem2  25978  chpchtlim  25983  rplogsumlem1  25988  dchrvmasumiflem1  26005  dchrisum0flblem2  26013  dchrisum0fno1  26015  dchrisum0lem2a  26021  dchrisum0lem3  26023  dirith  26033  mulog2sumlem1  26038  mulog2sumlem2  26039  log2sumbnd  26048  selberglem2  26050  logdivbnd  26060  selberg3lem1  26061  selberg4lem1  26064  pntrsumbnd2  26071  pntrlog2bndlem1  26081  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntibndlem3  26096  pntlemb  26101  pntlemn  26104  pntlemr  26106  pntlemj  26107  pntlemf  26109  pntlemo  26111  ostth2lem3  26139  ostth3  26142  footeq  26438  hlperpnel  26439  perpdragALT  26441  perpdrag  26442  colperp  26443  mideulem2  26448  opphllem  26449  opphllem3  26463  lmieu  26498  trgcopy  26518  sacgr  26545  acopyeu  26548  usgredgleordALT  26944  eucrctshift  27950  nvabs  28377  smcnlem  28402  ubthlem2  28576  minvecolem4  28585  htthlem  28622  normpyc  28851  nmophmi  29736  hstle  29935  hstles  29936  stlei  29945  f1rnen  30303  nnmulge  30401  fsumiunle  30473  wrdt2ind  30555  xrge0npcan  30609  trsp2cyc  30693  archirngz  30746  archiabllem1a  30748  archiabllem2a  30751  archiabllem2c  30752  ornglmulle  30806  orngrmulle  30807  drngdimgt0  30916  lbsdiflsp0  30922  madjusmdetlem2  30993  esumpinfval  31232  esumpinfsum  31236  esumpcvgval  31237  esum2d  31252  esumiun  31253  dya2icoseg  31435  omssubadd  31458  carsgsigalem  31473  carsggect  31476  carsgclctunlem3  31478  omsmeas  31481  eulerpartlems  31518  sgnmulsgn  31707  signsplypnf  31720  signsply0  31721  reprlt  31790  reprinfz1  31793  hgt750lemc  31818  hgt750lemf  31824  pthhashvtx  32272  resconn  32391  sinccvglem  32813  circum  32815  btwnxfr  33415  nn0prpwlem  33568  dnibndlem2  33716  unblimceq0  33744  poimirlem7  34781  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem3  34827  ftc1anc  34857  isbnd3  34945  cntotbnd  34957  bfp  34985  rrndstprj2  34992  1cvrjat  36493  3atlem1  36501  3atlem6  36506  llnmlplnN  36557  2llnjaN  36584  2lplnja  36637  dalem57  36747  dalawlem11  36899  dalawlem12  36900  lhp2lt  37019  lhpj1  37040  lhpm0atN  37047  4atexlemex2  37089  lautm  37112  cdleme17b  37305  cdleme20j  37336  cdleme30a  37396  cdlemg4c  37630  cdlemg17a  37679  cdlemg31c  37717  trljco  37758  cdlemk46  37966  dia2dimlem2  38083  cdlemm10N  38136  cdlemn10  38224  dihmeetlem1N  38308  dihglblem5apreN  38309  dihmeetlem15N  38339  mapdat  38685  rtprmirr  39074  fltnlta  39155  3cubeslem1  39161  irrapxlem1  39299  irrapxlem4  39302  pell1qrgaplem  39350  pellfundglb  39362  rmspecfund  39386  monotoddzzfi  39419  rmynn  39433  jm2.24nn  39436  jm2.17c  39439  jm2.24  39440  acongeq  39460  jm2.20nn  39474  jm2.26lem3  39478  jm2.27a  39482  jm2.27c  39484  rmydioph  39491  jm3.1lem2  39495  frlmpwfi  39578  areaquad  39703  rp-isfinite6  39764  frege129d  39988  leeq1d  40387  imo72b2  40406  cvgdvgrat  40525  radcnvrat  40526  hashnzfzclim  40534  isosctrlem1ALT  41148  cncmpmax  41169  iooabslt  41654  fmul01lt1lem2  41746  clim1fr1  41762  limcrecl  41790  climxrrelem  41910  liminflbuz2  41976  stoweidlem1  42167  stoweidlem11  42177  stoweidlem14  42180  stoweidlem24  42190  stoweidlem26  42192  wallispilem4  42234  wallispilem5  42235  stirlinglem1  42240  fourierdlem51  42323  fourierdlem65  42337  fouriersw  42397  2leaddle2  43379  sqrtpwpw2p  43547  lighneallem4a  43620  flnn0div2ge  44491  logbpw2m1  44525  amgmwlem  44801
  Copyright terms: Public domain W3C validator