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

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

Proof of Theorem eqbrtrd
StepHypRef Expression
1 eqbrtrd.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrd.1 . . 3 (𝜑𝐴 = 𝐵)
32breq1d 4850 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 248 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4841
This theorem is referenced by:  eqbrtrrd  4864  somin2  5739  en1b  8257  domunsncan  8296  fodomfi  8475  hartogslem1  8683  wemaplem2  8688  infdifsn  8798  carddomi2  9076  cdaun  9276  cda1dif  9280  mapcdaen  9288  cdaxpdom  9293  cdafi  9294  cdainf  9296  carden  9655  alephsuc3  9684  fpwwe2lem6  9739  fpwwe2lem7  9740  inar1  9879  rankcf  9881  lesub3d  10927  lbinfle  11260  supadd  11273  supmul  11277  rpnnen1lem3  12031  divge1  12108  xrmin1  12222  xrmin2  12223  ifle  12242  qbtwnxr  12245  xltnegi  12261  xleadd1a  12297  xlt2add  12304  xlemul1a  12332  xov1plusxeqvd  12537  ubmelm1fzo  12784  flflp1  12828  ceim1l  12866  ceilm1lt  12867  ceille  12869  quoremz  12874  quoremnn0ALT  12876  modlt  12899  modeqmodmin  12960  addmodlteq  12965  seqf1olem1  13059  bernneq  13209  discr  13220  faclbnd2  13294  faclbnd4lem3  13298  hashun2  13386  hashfun  13437  ccatsymb  13575  ccatrn  13582  sqrlem6  14207  sqrlem7  14208  rddif  14299  amgm2  14328  icodiamlt  14393  climconst  14493  rlimconst  14494  serclim0  14527  rlimcn1  14538  mulcn2  14545  reccn2  14546  o1mul  14564  o1rlimmul  14568  iserex  14606  climlec2  14608  iserge0  14610  climcau  14620  caucvgrlem  14622  caucvgr  14625  iseraltlem2  14632  iseraltlem3  14633  iseralt  14634  fsumabs  14751  o1fsum  14763  iserabs  14765  climfsum  14770  isumless  14795  climcndslem2  14800  divrcnv  14802  flo1  14804  supcvg  14806  georeclim  14821  geomulcvg  14825  cvgrat  14832  mertenslem1  14833  prodfclim1  14842  fprodge1  14942  fprodle  14943  efcvgfsum  15032  eftlub  15055  eflegeo  15067  tanhlt1  15106  tanhbnd  15107  ef01bndlem  15130  sin01bnd  15131  cos01bnd  15132  cos01gt0  15137  ruclem2  15177  ruclem3  15178  ruclem9  15183  ruclem11  15185  ruclem12  15186  bitsfzolem  15371  bitsfzo  15372  bitsinv1lem  15378  sadcaddlem  15394  mulgcd  15480  eucalglt  15513  lcmledvds  15527  lcmfledvds  15560  mulgcddvds  15583  coprmproddvdslem  15590  prmind2  15612  isprm5  15632  divdenle  15670  nonsq  15680  pythagtriplem4  15737  pclem  15756  pcpremul  15761  pczdvds  15780  pcprmpw2  15799  qexpz  15818  prmreclem4  15836  prmreclem5  15837  4sqlem10  15864  ramtub  15929  ramub2  15931  prmodvdslcmf  15964  prmgaplem8  15975  natpropd  16836  catciso  16957  p0le  17244  acsdomd  17382  qusgrp  17847  f1otrspeq  18064  pmtrfrn  18075  pmtrfconj  18083  symggen  18087  psgnunilem4  18114  oddvds2  18180  odcau  18216  pgpfi  18217  pgpssslw  18226  sylow3lem4  18242  efgred2  18363  frgp0  18370  odadd2  18449  oddvdssubg  18455  ablfac1c  18668  ablfac1eu  18670  pgpfaclem3  18680  isabvd  19020  abvsubtri  19035  mplsubrg  19645  coe1sfi  19787  cyggic  20124  mp2pm2mplem5  20824  en2top  20999  1stcrest  21466  2ndcrest  21467  hausmapdom  21513  ufilen  21943  xmetrtri2  22370  prdsxmetlem  22382  bl2in  22414  xblcntrps  22424  xblcntr  22425  ssblps  22436  ssbl  22437  blssps  22438  blss  22439  blcld  22519  methaus  22534  metustexhalf  22570  nmtri2  22640  tngngp3  22669  nrginvrcnlem  22704  nrginvrcn  22705  nmoi  22741  nmo0  22748  nmoid  22755  blcvx  22810  reperflem  22830  reconnlem2  22839  metdcnlem  22848  metdscn  22868  metnrmlem3  22873  mulc1cncf  22917  iccpnfhmeo  22953  cnheiborlem  22962  cnheibor  22963  lebnumii  22974  pcopt  23030  pcopt2  23031  pcoass  23032  nmoleub2lem  23122  nmoleub2lem3  23123  nmoleub2lem2  23124  ipcau2  23241  tchcphlem1  23242  nglmle  23308  trirn  23391  rrxdstprj1  23400  minveclem3  23408  ivthlem2  23429  ivthlem3  23430  ivth2  23432  ovollb  23456  ovolsslem  23461  ovollb2lem  23465  ovolctb  23467  ovoliunlem1  23479  ovolsca  23492  ovolicc1  23493  ovolicc2lem4  23497  nulmbl  23512  ioombl1lem4  23538  uniioovol  23556  uniioombllem3a  23561  uniioombllem4  23563  opnmbllem  23578  volcn  23583  volivth  23584  i1fadd  23672  i1fmul  23673  mbfi1fseqlem4  23695  mbfi1fseqlem5  23696  mbfi1fseqlem6  23697  itg2const2  23718  itg2seq  23719  itg2uba  23720  itg2split  23726  itg2monolem1  23727  itg2monolem3  23729  itg2i1fseq2  23733  itg2addlem  23735  itg2gt0  23737  itg2cnlem1  23738  itg2cnlem2  23739  itgless  23793  ibladdlem  23796  bddmulibl  23815  dveflem  23952  dvferm1lem  23957  dvferm2lem  23959  dvlip  23966  dvlipcn  23967  dvlip2  23968  dvle  23980  dvivthlem1  23981  lhop1lem  23986  dvcvx  23993  dvfsumabs  23996  dvfsumlem2  24000  dvfsumlem4  24002  dvfsumrlim2  24005  dvfsum2  24007  ftc1a  24010  ftc1lem4  24012  ftc1lem5  24013  deg1sub  24078  ply1divex  24106  deg1submon1p  24122  r1pdeglt  24128  dvdsq1p  24130  fta1glem2  24136  fta1g  24137  plyeq0lem  24176  dgrlt  24232  fta1lem  24272  aalioulem2  24298  aalioulem3  24299  aalioulem4  24300  aaliou3lem2  24308  aaliou3lem9  24315  taylply2  24332  ulmbdd  24362  ulmdvlem1  24364  mtest  24368  mtestbdd  24369  radcnvlem1  24377  radcnvle  24384  pserulm  24386  psercn  24390  pserdvlem2  24392  abelthlem2  24396  abelthlem5  24399  abelthlem7  24402  abelthlem8  24403  abelthlem9  24404  reeff1olem  24410  tangtx  24468  tanord  24495  efif1olem4  24502  logrnaddcl  24531  logcj  24562  logimul  24570  logneg2  24571  logdivlti  24576  divlogrlim  24591  logcnlem3  24600  logcnlem4  24601  efopn  24614  logtayllem  24615  logtayl  24616  cxpcn3lem  24698  cxpaddle  24703  abscxpbnd  24704  asinlem3  24808  asinneg  24823  asinsin  24829  atanlogaddlem  24850  atantan  24860  bndatandm  24866  atans2  24868  atantayl  24874  atantayl2  24875  atantayl3  24876  leibpi  24879  birthdaylem3  24890  rlimcnp  24902  efrlim  24906  cxplim  24908  cxp2lim  24913  cxploglim2  24915  divsqrtsumo1  24920  jensenlem2  24924  amgm  24927  logdifbnd  24930  harmonicbnd4  24947  fsumharmonic  24948  lgamgulmlem2  24966  lgamgulmlem3  24967  lgamgulmlem5  24969  lgambdd  24973  lgamcvg2  24991  ftalem1  25009  ftalem5  25013  basellem1  25017  basellem8  25024  ppip1le  25097  ppiltx  25113  sqff1o  25118  chtublem  25146  chpub  25155  logfaclbnd  25157  logfacrlim  25159  logexprlim  25160  mersenne  25162  bcmono  25212  bcmax  25213  bposlem2  25220  bposlem5  25223  lgslem3  25234  gausslemma2dlem1a  25300  lgsquadlem1  25315  lgsquadlem2  25316  2lgslem1c  25328  2sqblem  25366  chebbnd1  25371  chtppilimlem1  25372  chto1ub  25375  chpchtlim  25378  chpo1ubb  25380  rplogsumlem1  25383  rplogsumlem2  25384  rpvmasumlem  25386  dchrisumlem1  25388  dchrisumlem2  25389  dchrmusum2  25393  dchrvmasumlem2  25397  dchrvmasumlem3  25398  dchrvmasumiflem1  25400  dchrisum0flblem1  25407  dchrisum0fno1  25410  dchrisum0lem1b  25414  dchrisum0lem1  25415  dchrisum0lem2a  25416  dchrisum0lem2  25417  rplogsum  25426  mudivsum  25429  mulogsumlem  25430  mulog2sumlem1  25433  mulog2sumlem2  25434  vmalogdivsum2  25437  2vmadivsumlem  25439  selberglem2  25445  selberg2b  25451  logdivbnd  25455  selberg3lem1  25456  selberg3lem2  25457  selberg4lem1  25459  pntrmax  25463  pntrsumo1  25464  pntrlog2bndlem1  25476  pntrlog2bndlem2  25477  pntrlog2bndlem3  25478  pntrlog2bndlem4  25479  pntrlog2bndlem5  25480  pntrlog2bnd  25483  pntpbnd1a  25484  pntpbnd2  25486  pntibndlem2  25490  pntlemb  25496  pntlemg  25497  pntlemh  25498  pntlemr  25501  pntlemj  25502  pntlemf  25504  pntlemo  25506  pnt  25513  padicabv  25529  ostth2lem2  25533  ostth2lem3  25534  ostth3  25537  colperpexlem3  25834  mideulem2  25836  lnperpex  25905  trgcopy  25906  iscgra1  25912  brbtwn2  25995  colinearalglem4  25999  subupgr  26391  crctcshwlkn0lem1  26927  nvabs  27852  nvge0  27853  smcnlem  27877  nmblolbii  27979  blocnilem  27984  siii  28033  ubthlem2  28052  minvecolem3  28057  htthlem  28099  bcsiALT  28361  bcs3  28365  chscllem4  28824  0cnop  29163  0cnfn  29164  nmbdoplbi  29208  nmcoplbi  29212  nmophmi  29215  nmbdfnlbi  29233  nmcfnlbi  29236  nlelchi  29245  riesz1  29249  cnlnadjlem2  29252  nmopadjlei  29272  nmoptrii  29278  nmopcoi  29279  nmopcoadji  29285  unierri  29288  branmfn  29289  pjs14i  29394  hstle  29414  cdj3lem2b  29621  xlt2addrd  29847  eliccelico  29863  elicoelioo  29864  ltesubnnd  29892  archirngz  30065  archiabllem2c  30071  madjusmdetlem2  30216  locfinref  30230  sqsscirc1  30276  tpr2rico  30280  esumcst  30447  esumgect  30474  esum2d  30477  measunl  30601  measiun  30603  omssubaddlem  30683  omssubadd  30684  carsgsigalem  30699  carsgclctunlem2  30703  pmeasmono  30708  eulerpartlemgc  30746  eulerpartlemb  30752  ballotlemsel1i  30896  ballotlemro  30906  sgnsub  30928  signsplypnf  30949  signsply0  30950  signsvtn  30983  signsvfnn  30985  hgt750lemd  31048  logdivsqrle  31050  erdsze2lem1  31505  sinccvglem  31885  divcnvlin  31937  iprodefisum  31946  faclimlem2  31949  nosep1o  32150  nodense  32160  fnemeet1  32679  dnibndlem10  32791  dnibndlem11  32792  dnibnd  32795  knoppcnlem4  32800  knoppcnlem6  32802  unblimceq0lem  32811  unblimceq0  32812  unbdqndv2lem1  32814  unbdqndv2lem2  32815  knoppndvlem11  32827  knoppndvlem12  32828  knoppndvlem14  32830  knoppndvlem15  32831  knoppndvlem17  32833  knoppndvlem18  32834  knoppndvlem19  32835  knoppndvlem21  32837  ltflcei  33707  ptrecube  33719  poimirlem16  33735  poimirlem17  33736  poimirlem29  33748  broucube  33753  opnmbllem0  33755  mblfinlem2  33757  mblfinlem3  33758  ismblfin  33760  itg2addnclem  33770  itg2addnclem2  33771  itg2addnclem3  33772  itg2addnc  33773  ibladdnclem  33775  ftc1cnnclem  33792  ftc1cnnc  33793  ftc1anc  33802  geomcau  33863  prdsbnd  33900  cntotbnd  33903  heiborlem4  33921  rrndstprj2  33938  rrncmslem  33939  rrnequiv  33942  iccbnd  33947  cvlcvr1  35116  cvrat3  35219  dalem25  35475  cdlema1N  35568  dalawlem3  35650  dalawlem4  35651  dalawlem5  35652  dalawlem6  35653  dalawlem7  35654  dalawlem9  35656  dalawlem11  35658  dalawlem12  35659  lhp2lt  35778  lhpmcvr  35800  4atexlemcnd  35849  lautj  35870  trlle  35962  trlval3  35965  trlval4  35966  cdleme0moN  36003  cdleme13  36050  cdleme15  36056  cdleme19b  36082  cdleme20e  36091  cdleme20j  36096  cdleme22e  36122  cdleme22eALTN  36123  cdleme26fALTN  36140  cdleme26f  36141  cdleme27N  36147  cdleme41sn3a  36211  cdleme46fsvlpq  36283  cdlemeg46vrg  36305  cdlemg4  36395  cdlemg7N  36404  cdlemg9a  36410  cdlemg11b  36420  cdlemg12a  36421  trljco  36518  tendoidcl  36547  tendococl  36550  tendopltp  36558  tendo0tp  36567  tendoicl  36574  cdlemi2  36597  cdlemk5a  36613  cdlemk5  36614  cdlemk12  36628  cdlemkole  36631  cdlemk14  36632  cdlemk12u  36650  cdlemk37  36692  cdlemk39s-id  36718  cdlemk49  36729  cdlemk39u1  36745  cdlemk39u  36746  dian0  36817  cdlemm10N  36896  cdlemn2  36973  cdlemn10  36984  dihord1  36996  dihord10  37001  dihmeetlem4preN  37084  dihmeetlem18N  37102  dihmeetlem20N  37104  dihjatc  37195  mapdcnvatN  37444  lzenom  37832  irrapxlem2  37886  irrapxlem3  37887  irrapxlem5  37889  pellexlem2  37893  pell14qrgt0  37922  pellfundlb  37947  pellfundex  37949  pellfund14  37961  rmspecsqrtnq  37969  jm2.24nn  38024  jm2.17a  38025  jm2.17b  38026  congabseq  38039  acongrep  38045  acongeq  38048  jm2.26lem3  38066  jm2.27a  38070  jm2.27c  38072  hbtlem2  38192  dgraaub  38216  idomodle  38272  relexpxpmin  38506  frege102d  38543  hashnzfzclim  39018  binomcxplemfrat  39047  binomcxplemnotnn0  39052  suprnmpt  39841  mpct  39877  rnmptbddlem  39936  dstregt0  39972  lefldiveq  39984  fzisoeu  39992  upbdrech  39997  ssfiunibd  40001  fzdifsuc2  40002  xadd0ge  40013  supxrgere  40026  supxrge  40031  suplesup  40032  xrlexaddrp  40045  infxrunb2  40061  infleinflem2  40064  reclt0d  40084  infrpgernmpt  40171  ioondisj2  40195  iccshift  40222  iooshift  40226  fmul01  40289  fmul01lt1lem1  40293  fmul01lt1lem2  40294  climrec  40312  climsuse  40317  mullimc  40325  mullimcf  40332  constlimc  40333  idlimc  40335  divcnvg  40336  limcperiod  40337  limcrecl  40338  lptioo2  40340  lptioo1  40341  islpcn  40348  lptre2pt  40349  limcleqr  40353  neglimc  40356  addlimc  40357  0ellimcdiv  40358  limclner  40360  climleltrp  40385  limsuplesup  40408  limsupmnflem  40429  supcnvlimsupmpt  40450  0cnv  40451  xlimconst  40528  sinaover2ne0  40556  cncfshift  40564  cncfperiod  40569  cncfioobdlem  40586  cncfioobd  40587  fperdvper  40610  dvdivbd  40615  dvbdfbdioolem1  40620  dvbdfbdioolem2  40621  ioodvbdlimc1lem1  40623  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvnmul  40635  dvnprodlem1  40638  itgiccshift  40672  itgperiod  40673  ismbl3  40679  ovolsplit  40681  stoweidlem1  40694  stoweidlem11  40704  stoweidlem13  40706  stoweidlem14  40707  stoweidlem16  40709  stoweidlem21  40714  stoweidlem25  40718  stoweidlem26  40719  stoweidlem36  40729  stoweidlem38  40731  stoweidlem41  40734  stoweidlem42  40735  stoweidlem45  40738  stoweidlem48  40741  stoweidlem52  40745  stoweidlem62  40755  wallispilem3  40760  stirlinglem5  40771  stirlinglem6  40772  stirlinglem7  40773  stirlinglem10  40776  stirlinglem12  40778  stirlinglem15  40781  dirkercncflem1  40796  fourierdlem10  40810  fourierdlem12  40812  fourierdlem15  40815  fourierdlem16  40816  fourierdlem19  40819  fourierdlem20  40820  fourierdlem21  40821  fourierdlem22  40822  fourierdlem24  40824  fourierdlem30  40830  fourierdlem37  40837  fourierdlem39  40839  fourierdlem40  40840  fourierdlem41  40841  fourierdlem42  40842  fourierdlem47  40846  fourierdlem48  40847  fourierdlem49  40848  fourierdlem50  40849  fourierdlem52  40851  fourierdlem54  40853  fourierdlem60  40859  fourierdlem61  40860  fourierdlem63  40862  fourierdlem64  40863  fourierdlem68  40867  fourierdlem71  40870  fourierdlem72  40871  fourierdlem73  40872  fourierdlem74  40873  fourierdlem75  40874  fourierdlem76  40875  fourierdlem77  40876  fourierdlem78  40877  fourierdlem79  40878  fourierdlem81  40880  fourierdlem82  40881  fourierdlem83  40882  fourierdlem84  40883  fourierdlem87  40886  fourierdlem92  40891  fourierdlem93  40892  fourierdlem94  40893  fourierdlem101  40900  fourierdlem102  40901  fourierdlem103  40902  fourierdlem104  40903  fourierdlem111  40910  fourierdlem112  40911  fourierdlem113  40912  fourierdlem114  40913  sqwvfoura  40921  sqwvfourb  40922  fouriersw  40924  elaa2lem  40926  etransclem23  40950  etransclem28  40955  etransclem32  40959  etransclem35  40962  etransclem48  40975  qndenserrnbllem  40990  rrnprjdstle  40997  ioorrnopnlem  41000  ioorrnopnxrlem  41002  salexct  41028  sge0fsum  41080  sge0supre  41082  sge0rnbnd  41086  sge0lefi  41091  sge0lessmpt  41092  sge0ltfirp  41093  sge0prle  41094  sge0resrnlem  41096  sge0le  41100  sge0split  41102  sge0iunmptlemre  41108  sge0iunmpt  41111  sge0isum  41120  sge0xaddlem1  41126  sge0xaddlem2  41127  sge0xadd  41128  sge0reuz  41140  sge0reuzb  41141  meaunle  41157  meaiunlelem  41161  voliunsge0lem  41165  meaiuninc  41174  meaiininclem  41179  omeunle  41209  omeiunle  41210  omelesplit  41211  omeiunltfirp  41212  carageniuncllem2  41215  caratheodorylem2  41220  caragencmpl  41228  ovnlecvr  41251  ovncvrrp  41257  ovnsubaddlem1  41263  ovnsubadd  41265  hoidmv1lelem1  41284  hoidmv1lelem2  41285  hoidmv1le  41287  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem5  41292  hoidmvle  41293  ovnhoilem1  41294  ovnlecvr2  41303  ovncvr2  41304  hoiqssbllem2  41316  hspmbllem2  41320  hspmbllem3  41321  ovnsplit  41341  ovolval5lem1  41345  vonioolem1  41373  vonioolem2  41374  vonicclem1  41376  vonicclem2  41377  pimconstlt1  41394  smflimlem2  41459  smflimlem4  41461  smfmullem1  41477  smfsuplem1  41496  smflimsuplem4  41508  smflimsuplem5  41509  iccpartltu  41933  iccpartleu  41936  pgrple2abl  42711  difmodm1lt  42882  nnpw2blen  42939  dignn0flhalflem1  42974
  Copyright terms: Public domain W3C validator