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

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

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32breq2d 4697 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 222 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:  breqtrrd  4713  syl5breq  4722  domunsn  8151  mapdom2  8172  phplem4  8183  mapfien2  8355  wemaplem2  8493  infdifsn  8592  cantnff  8609  infxpenlem  8874  pwcda1  9054  pwcdadom  9076  infmap2  9078  ssfin4  9170  canthp1lem1  9512  nqereq  9795  ltexnq  9835  ltbtwnnq  9838  add20  10578  mullt0  10585  ltm1  10901  recgt0  10905  prodgt0  10906  prodge0  10908  ltmul1a  10910  mulge0b  10931  recp1lt1  10959  recreclt  10960  ledivp1  10963  ledivp1i  10987  ltdivp1i  10988  eluzmn  11732  ltaddrp2d  11944  mul2lt0bi  11974  xleadd1a  12121  xov1plusxeqvd  12356  fz01en  12407  fzonmapblen  12553  fladdz  12666  flhalf  12671  fldiv  12699  modsubdir  12779  fzen2  12808  serle  12896  ltexp2a  12952  leexp2a  12956  exple1  12960  expubnd  12961  bernneq  13030  expmulnbnd  13036  discr1  13040  discr  13041  faclbnd6  13126  hashfz  13252  hashfun  13262  seqcoll  13286  sqeqd  13950  sqrlem7  14033  sqrtge0  14042  sqrtneglem  14051  abslt  14098  absle  14099  abstri  14114  rlimge0  14356  reccn2  14371  climaddc2  14410  isercolllem1  14439  caucvgrlem  14447  summolem2a  14490  isumge0  14541  fsumle  14575  fsumlt  14576  o1fsum  14589  supcvg  14632  expcnv  14640  geolim  14645  geolim2  14646  georeclim  14647  geo2lim  14650  mertenslem1  14660  mertens  14662  prodmolem2a  14708  efcllem  14852  ef0lem  14853  efgt0  14877  eftlub  14883  eflt  14891  sinbnd  14954  cosbnd  14955  ef01bndlem  14958  sin01gt0  14964  cos01gt0  14965  sin02gt0  14966  eirrlem  14976  rpnnen2lem11  14997  rpnnen2lem12  14998  ruclem11  15013  dvdssub2  15070  dvdsadd2b  15075  dvdsexp  15096  3dvds  15099  3dvdsOLD  15100  opoe  15134  bitsfzolem  15203  bitsinv1lem  15210  bezoutlem4  15306  dvdsgcd  15308  dvdsmulgcd  15321  bezoutr1  15329  nn0seqcvgd  15330  rpmulgcd2  15417  qredeq  15418  rpdvds  15421  prmind2  15445  divdenle  15504  hashdvds  15527  phimullem  15531  eulerthlem2  15534  prmdiveq  15538  prmdivdiv  15539  pythagtriplem4  15571  pythagtriplem10  15572  pythagtriplem19  15585  iserodd  15587  pcpre1  15594  pcadd2  15641  qexpz  15652  expnprm  15653  oddprmdvds  15654  pockthlem  15656  prmreclem2  15668  prmreclem3  15669  4sqlem7  15695  4sqlem10  15698  4sqlem11  15706  4sqlem12  15707  4sqlem14  15709  4sqlem15  15710  4sqlem16  15711  0ram  15771  ffthiso  16636  latmlej12  17138  qusgrp  17696  pgpfi1  18056  sylow1lem4  18062  sylow1lem5  18063  odcau  18065  pgpfi  18066  pgpssslw  18075  sylow3lem4  18091  sylow3lem6  18093  efgsfo  18198  frgp0  18219  odadd1  18297  odadd2  18298  odadd  18299  gexexlem  18301  lt6abl  18342  gsumzsubmcl  18364  pwsgsum  18424  dprd2dlem1  18486  dprd2d2  18489  ablfacrplem  18510  ablfacrp  18511  ablfacrp2  18512  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem3a  18521  ablfaclem2  18531  dvdsrid  18697  dvdsrtr  18698  dvdsrneg  18700  unitmulcl  18710  unitgrp  18713  unitnegcl  18727  isdrng2  18805  subrguss  18843  subrgunit  18846  abvsubtri  18883  fidomndrnglem  19354  psrbaglesupp  19416  gzrngunit  19860  prmirredlem  19889  znidomb  19958  frlmgsum  20159  invrvald  20530  psmetsym  22162  psmettri  22163  mettri2  22193  xmetsym  22199  xmettri  22203  prdsxmetlem  22220  xblss2ps  22253  xblss2  22254  blhalf  22257  xmsge0  22315  ngptgp  22487  nrginvrcnlem  22542  nmoeq0  22587  cnmet  22622  blcvx  22648  opnreen  22681  metdcnlem  22686  metdstri  22701  metdsle  22702  metnrmlem1  22709  metnrmlem3  22711  lebnumlem1  22807  pi1inv  22898  cphnmf  23041  ipge0  23044  ipcau2  23079  tchcphlem1  23080  csbren  23228  minveclem2  23243  minveclem3  23246  ovolssnul  23301  ovolctb  23304  ovolunnul  23314  ovoliunlem1  23316  ovoliun2  23320  ovoliunnul  23321  ioombl1lem4  23375  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  uniioombl  23403  volcn  23420  vitalilem2  23423  vitalilem5  23426  itg1lea  23524  mbfi1fseqlem6  23532  mbfi1flimlem  23534  itg2eqa  23557  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2cnlem2  23574  iblabsr  23641  iblmulc2  23642  dveflem  23787  dvef  23788  dvferm2lem  23794  dvlip  23801  c1liplem1  23804  dveq0  23808  dvlt0  23813  dvivthlem1  23816  lhop1  23822  dvfsumle  23829  dvfsumlem4  23837  dvfsumrlim3  23841  dvfsum2  23842  ftc1a  23845  ftc1lem4  23847  deg1add  23908  ply1divex  23941  ply1rem  23968  fta1glem2  23971  fta1blem  23973  ig1pdvds  23981  plyeq0lem  24011  dgrcolem2  24075  plydivlem4  24096  plyrem  24105  fta1lem  24107  aalioulem3  24134  aaliou2b  24141  aaliou3lem3  24144  aaliou3lem8  24145  ulmcn  24198  ulmdvlem1  24199  itgulm  24207  pserulm  24221  pserdvlem2  24227  abelthlem2  24231  abelthlem5  24234  abelthlem6  24235  abelthlem7  24237  abelthlem8  24238  abelthlem9  24239  sinq12gt0  24304  sinq34lt0t  24306  cosq14gt0  24307  cosq14ge0  24308  efif1olem3  24335  argimgt0  24403  argimlt0  24404  logneg2  24406  logcnlem3  24435  logcnlem4  24436  logtayllem  24450  logtayl2  24453  cxpsqrtlem  24493  cxpsqrt  24494  cxpaddlelem  24537  abscxpbnd  24539  loglesqrt  24544  ang180lem2  24585  atanlogaddlem  24685  atanlogsublem  24687  atantan  24695  atans2  24703  atantayl  24709  leibpi  24714  log2tlbnd  24717  birthdaylem2  24724  birthdaylem3  24725  cxp2limlem  24747  jensenlem2  24759  jensen  24760  logdiflbnd  24766  emcllem2  24768  emcllem4  24770  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem2  24801  lgamgulm2  24807  lgambdd  24808  lgamucov  24809  lgamcvglem  24811  lgamcvg2  24826  gamcvg  24827  wilthlem3  24841  basellem1  24852  basellem3  24854  basellem4  24855  fsumdvdsdiaglem  24954  dvdsppwf1o  24957  dvdsmulf1o  24965  chteq0  24979  chtub  24982  chpub  24990  logfacubnd  24991  logfaclbnd  24992  logexprlim  24995  perfectlem2  25000  dchrfi  25025  bclbnd  25050  bposlem1  25054  bposlem3  25056  bposlem4  25057  bposlem6  25059  lgslem1  25067  lgsqrlem2  25117  lgsqrlem4  25119  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  2sqlem3  25190  2sqlem4  25191  2sqlem8  25196  2sqlem11  25199  chebbnd1lem2  25204  chebbnd1lem3  25205  chtppilimlem1  25207  chpchtlim  25213  vmadivsum  25216  vmadivsumb  25217  rpvmasumlem  25221  dchrisumlem2  25224  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  dchrisum0lem1  25250  dchrisum0lem2a  25251  mudivsum  25264  mulogsumlem  25265  mulog2sumlem2  25269  vmalogdivsum2  25272  selberglem2  25280  selbergb  25283  selberg2b  25286  logdivbnd  25290  selberg3lem1  25291  selberg3lem2  25292  selberg4lem1  25294  pntrmax  25298  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6a  25316  pntrlog2bndlem6  25317  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem1  25323  pntibndlem2  25325  pntlemb  25331  pntlemq  25335  pntlemr  25336  pntlemj  25337  pntlemk  25340  qabvle  25359  padicabvcxp  25366  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth3  25372  legtrid  25531  legov3  25538  krippenlem  25630  mideulem2  25671  midex  25674  opphllem5  25688  opphllem6  25689  opphl  25691  lmieu  25721  lmiisolem  25733  ttgcontlem1  25810  colinearalglem4  25834  axpaschlem  25865  axcontlem7  25895  nbfusgrlevtxm2  26324  clwlksndivn  27059  eucrct2eupth  27223  nvge0  27656  smcnlem  27680  nmoub3i  27756  nmoub2i  27757  nmlno0lem  27776  minvecolem2  27859  htthlem  27902  norm3dif2  28136  bcs2  28167  chscllem2  28625  eigposi  28823  nmopub2tALT  28896  nmfnleub2  28913  nmlnop0iALT  28982  riesz1  29052  cnlnadjlem2  29055  nmopcoadji  29088  leopsq  29116  leopmul  29121  leopnmid  29125  nmopleid  29126  opsqrlem6  29132  0leopj  29173  hstle1  29213  strlem3a  29239  mdslmd4i  29320  cvexchlem  29355  cdj1i  29420  le2halvesd  29648  xlt2addrd  29651  fsumub  29702  2sqcoprm  29775  2sqmod  29776  archiabllem1a  29873  archiabllem2a  29876  archiabllem2c  29877  xrge0tsmsd  29913  orngsqr  29932  ornglmulle  29933  orngrmulle  29934  orng0le1  29940  fzto1st1  29980  metideq  30064  metider  30065  sqsscirc1  30082  esummono  30244  esumpad2  30246  esumle  30248  esumlef  30252  esumcst  30253  esumrnmpt2  30258  esum2d  30283  aean  30435  dya2ub  30460  dya2icoseg  30467  omssubadd  30490  inelcarsg  30501  carsgsigalem  30505  carsggect  30508  carsgclctunlem2  30509  eulerpartlemb  30558  fibp1  30591  sgnmulsgp  30740  signsplypnf  30755  signsply0  30756  fdvposlt  30805  fdvposle  30807  reprgt  30827  logdivsqrle  30856  hgt750lemb  30862  hgt750leme  30864  tgoldbachgtde  30866  subfacval3  31297  sconnpht2  31346  sconnpi1  31347  resconn  31354  snmlff  31437  sinccvglem  31692  faclimlem2  31756  btwnouttr2  32254  dnibndlem5  32597  dnibndlem7  32599  dnibndlem8  32600  dnibndlem9  32601  dnibndlem10  32602  dnibnd  32606  knoppcnlem4  32611  knoppcnlem9  32616  unbdqndv2lem1  32625  unbdqndv2lem2  32626  knoppndvlem11  32638  knoppndvlem12  32639  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem18  32645  knoppndvlem19  32646  knoppndvlem21  32648  ltflcei  33527  poimirlem9  33548  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  volsupnfl  33584  itg2addnclem  33591  itg2addnclem3  33593  iblmulc2nc  33605  bddiblnc  33610  ftc1cnnclem  33613  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc2nc  33624  dvasin  33626  geomcau  33685  bfplem2  33752  rrncmslem  33761  rrnequiv  33764  lsatcvatlem  34654  islshpcv  34658  atlatmstc  34924  cvlsupr7  34953  cvrval3  35017  cvrval5  35019  cvrexchlem  35023  atcvrj1  35035  cvrat3  35046  cvrat4  35047  atbtwn  35050  1cvratex  35077  hlatexch4  35085  3atlem1  35087  3atlem2  35088  atcvrlln2  35123  atcvrlln  35124  lplnllnneN  35160  llncvrlpln2  35161  4atlem3b  35202  lplncvrlvol2  35219  dalemswapyz  35260  dalemswapyzps  35294  dalem25  35302  dalem39  35315  dalem58  35334  dalem59  35335  lneq2at  35382  lncvrat  35386  dalawlem2  35476  dalawlem3  35477  dalawlem4  35478  dalawlem6  35480  dalawlem9  35483  dalawlem11  35485  dalawlem12  35486  lhpocnle  35620  lhpmcvr3  35629  lhpmcvr5N  35631  lhpmcvr6N  35632  4atexlemunv  35670  4atexlemc  35673  4atexlemex2  35675  lautm  35698  cdlemc2  35797  cdleme5  35845  cdleme11j  35872  cdleme16b  35884  cdlemednpq  35904  cdleme19e  35912  cdleme20i  35922  cdleme22a  35945  cdleme22cN  35947  cdleme22d  35948  cdleme22e  35949  cdleme22eALTN  35950  cdleme22f  35951  cdleme23c  35956  cdleme30a  35983  cdleme35a  36053  cdleme35b  36055  cdleme42h  36087  cdlemeg46rgv  36133  cdlemg8b  36233  cdlemg12e  36252  cdlemg13a  36256  cdlemg17pq  36277  cdlemg18c  36285  cdlemg19  36289  cdlemg21  36291  cdlemg31d  36305  cdlemg33a  36311  tendoid  36378  cdlemk4  36439  cdlemki  36446  cdlemk10  36448  cdlemksv2  36452  cdlemk12  36455  cdlemk14  36459  cdlemk15  36460  cdlemk1u  36464  cdlemk5u  36466  cdlemk12u  36477  cdlemk45  36552  cdlemk48  36555  dia2dimlem1  36670  dia2dimlem2  36671  dia2dimlem3  36672  cdlemm10N  36724  cdlemn2  36801  dihjustlem  36822  dihglbcpreN  36906  dihmeetlem3N  36911  irrapxlem1  37703  pell1qrgaplem  37754  pell1qrgap  37755  monotoddzzfi  37824  jm2.24nn  37843  congtr  37849  congmul  37851  congsub  37854  fzmaxdif  37865  acongeq  37867  jm2.20nn  37881  jm2.25  37883  hbtlem4  38013  dgrsub2  38022  mpaaeu  38037  idomsubgmo  38093  leeq2d  38773  int-sqgeq0d  38806  int-ineqmvtd  38811  cvgdvgrat  38829  radcnvrat  38830  hashnzfzclim  38838  dvconstbi  38850  binomcxplemdvbinom  38869  isosctrlem1ALT  39484  mulltgt0  39495  rnmptbd2lem  39777  oddfl  39803  2timesgt  39814  lt3addmuld  39829  lt4addmuld  39834  supxrgere  39862  supxrgelem  39866  supxrge  39867  xadd0ge2  39870  infrpge  39880  xrlexaddrp  39881  xralrple2  39883  infxr  39896  infleinflem1  39899  infleinflem2  39900  infleinf  39901  xralrple4  39902  xralrple3  39903  recnnltrp  39906  rpgtrecnn  39910  xrralrecnnge  39926  rexabslelem  39958  infrnmptle  39963  supminfxr  40007  xrpnf  40029  iccshift  40062  iooshift  40066  ressiocsup  40099  ressioosup  40100  fsumnncl  40121  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  mccllem  40147  climrec  40153  climexp  40155  climneg  40160  limcrecl  40179  sumnnodd  40180  lptioo2  40181  lptioo1  40182  ltmod  40188  lptre2pt  40190  0ellimcdiv  40199  limclner  40201  fnlimcnv  40217  climinf2lem  40256  limsupubuzlem  40262  limsup10exlem  40322  limsupgtlem  40327  dfxlim2v  40391  cncficcgt0  40419  cncfioobdlem  40427  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvdsn1add  40472  dvnxpaek  40475  dvnmul  40476  dvnprodlem1  40479  itgiccshift  40514  itgperiod  40515  sublevolico  40519  ismbl3  40521  ovolsplit  40523  ismbl4  40528  stoweidlem1  40536  stoweidlem11  40546  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  stoweidlem38  40573  stoweidlem42  40577  stoweidlem51  40586  stoweidlem59  40594  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  stirlinglem13  40621  stirlinglem15  40623  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem4  40646  fourierdlem10  40652  fourierdlem11  40653  fourierdlem15  40657  fourierdlem20  40662  fourierdlem25  40667  fourierdlem26  40668  fourierdlem30  40672  fourierdlem37  40679  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem44  40686  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem52  40693  fourierdlem54  40695  fourierdlem60  40701  fourierdlem61  40702  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem81  40722  fourierdlem84  40725  fourierdlem87  40728  fourierdlem92  40733  fourierdlem93  40734  fourierdlem101  40742  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  etransclem19  40788  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem27  40796  etransclem32  40801  etransclem35  40804  etransclem48  40817  qndenserrnbllem  40832  ioorrnopnlem  40842  ioorrnopnxrlem  40844  fsumlesge0  40912  sge0cl  40916  sge0supre  40924  sge0less  40927  sge0gerp  40930  sge0ltfirp  40935  sge0le  40942  sge0ltfirpmpt  40943  sge0split  40944  sge0rpcpnf  40956  sge0ltfirpmpt2  40961  sge0isum  40962  sge0xaddlem1  40968  sge0pnffigtmpt  40975  sge0pnffsumgt  40977  sge0gtfsumgt  40978  sge0seq  40981  nnfoctbdjlem  40990  meassle  40998  meaiuninclem  41015  meaiininclem  41021  omeiunle  41052  omeiunltfirp  41054  carageniuncllem2  41057  carageniuncl  41058  omess0  41069  hoicvr  41083  ovnlerp  41097  ovnsubaddlem1  41105  hsphoidmvle2  41120  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem5  41134  ovnhoilem2  41137  ovnhoi  41138  hoidifhspdmvle  41155  hoiqssbllem2  41158  hspmbllem2  41162  hspmbllem3  41163  hspmbl  41164  vonioolem2  41216  vonicclem2  41219  smfaddlem1  41292  smflimlem2  41301  smflimlem4  41303  smfmullem1  41319  smfinflem  41344  smflimsuplem4  41350  smflimsuplem8  41354  perfectALTVlem2  41956  nnpw2blen  42699
  Copyright terms: Public domain W3C validator