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

Theorem eqbrtrd 4472
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 4462 . 2
41, 3mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  eqbrtrrd  4474  somin2  5410  en1b  7603  domunsncan  7637  fodomfi  7819  hartogslem1  7988  wemaplem2  7993  infdifsn  8094  carddomi2  8372  cdaun  8573  cda1dif  8577  mapcdaen  8585  cdaxpdom  8590  cdafi  8591  cdainf  8593  carden  8947  alephsuc3  8976  fpwwe2lem6  9034  fpwwe2lem7  9035  inar1  9174  rankcf  9176  lbinfmle  10523  supmul  10536  rpnnen1lem3  11239  xrmin1  11407  xrmin2  11408  ifle  11425  qbtwnxr  11428  xltnegi  11444  xleadd1a  11474  xlt2add  11481  xlemul1a  11509  xov1plusxeqvd  11695  ubmelm1fzo  11908  flflp1  11944  ceim1l  11974  ceilm1lt  11975  ceille  11977  quoremz  11982  quoremnn0ALT  11984  modlt  12006  modeqmodmin  12056  seqf1olem1  12146  bernneq  12292  discr  12303  faclbnd2  12369  faclbnd4lem3  12373  hashun2  12451  hashfun  12495  ccatsymb  12600  ccatrn  12606  lswccat0lsw  12608  sqrlem6  13081  sqrlem7  13082  rddif  13173  amgm2  13202  climconst  13366  rlimconst  13367  serclim0  13400  rlimcn1  13411  mulcn2  13418  reccn2  13419  o1mul  13437  o1rlimmul  13441  iserex  13479  climlec2  13481  iserge0  13483  climcau  13493  caucvgrlem  13495  caucvgr  13498  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  fsumabs  13615  o1fsum  13627  iserabs  13629  climfsum  13634  isumless  13657  climcndslem2  13662  divrcnv  13664  flo1  13666  supcvg  13667  georeclim  13681  geomulcvg  13685  cvgrat  13692  mertenslem1  13693  prodfclim1  13702  efcvgfsum  13821  eftlub  13844  eflegeo  13856  tanhlt1  13895  tanhbnd  13896  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  cos01gt0  13926  ruclem2  13965  ruclem3  13966  ruclem9  13971  ruclem11  13973  ruclem12  13974  bitsfzolem  14084  bitsfzo  14085  bitsinv1lem  14091  sadcaddlem  14107  mulgcd  14184  eucalglt  14214  prmind2  14228  mulgcddvds  14245  isprm5  14253  divdenle  14282  nonsq  14292  pythagtriplem4  14343  pclem  14362  pcpremul  14367  pczdvds  14386  pcprmpw2  14405  qexpz  14420  prmreclem4  14437  prmreclem5  14438  4sqlem10  14465  ramtub  14530  ramub2  14532  natpropd  15345  catciso  15434  p0le  15673  acsdomd  15811  qusgrp  16256  f1otrspeq  16472  pmtrfrn  16483  pmtrfconj  16491  symggen  16495  psgnunilem4  16522  oddvds2  16588  odcau  16624  pgpfi  16625  pgpssslw  16634  sylow3lem4  16650  efgred2  16771  frgp0  16778  odadd2  16855  oddvdssubg  16861  ablfac1c  17122  ablfac1eu  17124  pgpfaclem3  17134  isabvd  17469  abvsubtri  17484  mplsubrg  18102  coe1sfi  18252  cyggic  18611  mp2pm2mplem5  19311  en2top  19487  1stcrest  19954  2ndcrest  19955  hausmapdom  20001  ufilen  20431  xmetrtri2  20859  prdsxmetlem  20871  bl2in  20903  xblcntrps  20913  xblcntr  20914  ssblps  20925  ssbl  20926  blssps  20927  blss  20928  blcld  21008  methaus  21023  metustexhalfOLD  21066  metustexhalf  21067  nrginvrcnlem  21199  nrginvrcn  21200  nmoi  21235  nmo0  21242  nmoid  21249  blcvx  21303  reperflem  21323  reconnlem2  21332  metdcnlem  21341  metdscn  21360  metnrmlem3  21365  mulc1cncf  21409  iccpnfhmeo  21445  cnheiborlem  21454  cnheibor  21455  lebnumii  21466  pcopt  21522  pcopt2  21523  pcoass  21524  nmoleub2lem  21597  nmoleub2lem3  21598  nmoleub2lem2  21599  ipcau2  21677  tchcphlem1  21678  trirn  21827  rrxdstprj1  21836  minveclem3  21844  ivthlem2  21864  ivthlem3  21865  ivth2  21867  ovollb  21890  ovolsslem  21895  ovollb2lem  21899  ovolctb  21901  ovoliunlem1  21913  ovolsca  21926  ovolicc1  21927  ovolicc2lem4  21931  nulmbl  21946  ioombl1lem4  21971  uniioovol  21988  uniioombllem3a  21993  uniioombllem4  21995  opnmbllem  22010  volcn  22015  volivth  22016  i1fadd  22102  i1fmul  22103  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2split  22156  itg2monolem1  22157  itg2monolem3  22159  itg2i1fseq2  22163  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itgless  22223  ibladdlem  22226  bddmulibl  22245  dveflem  22380  dvferm1lem  22385  dvferm2lem  22387  dvlip  22394  dvlipcn  22395  dvlip2  22396  dvle  22408  dvivthlem1  22409  lhop1lem  22414  dvcvx  22421  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim2  22433  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  ftc1lem5  22441  deg1sub  22509  ply1divex  22537  deg1submon1p  22553  r1pdeglt  22559  dvdsq1p  22561  fta1glem2  22567  fta1g  22568  plyeq0lem  22607  dgrlt  22663  fta1lem  22703  aalioulem2  22729  aalioulem3  22730  aalioulem4  22731  aaliou3lem2  22739  aaliou3lem9  22746  taylply2  22763  ulmbdd  22793  ulmdvlem1  22795  mtest  22799  mtestbdd  22800  radcnvlem1  22808  radcnvle  22815  pserulm  22817  psercn  22821  pserdvlem2  22823  abelthlem2  22827  abelthlem5  22830  abelthlem7  22833  abelthlem8  22834  abelthlem9  22835  reeff1olem  22841  tangtx  22898  tanord  22925  efif1olem4  22932  logrnaddcl  22962  logcj  22991  logimul  22999  logneg2  23000  logdivlti  23005  divlogrlim  23016  logcnlem3  23025  logcnlem4  23026  efopn  23039  logtayllem  23040  logtayl  23041  cxpcn3lem  23121  cxpaddle  23126  abscxpbnd  23127  asinlem3  23202  asinneg  23217  asinsin  23223  atanlogaddlem  23244  atantan  23254  bndatandm  23260  atans2  23262  atantayl  23268  atantayl2  23269  atantayl3  23270  leibpi  23273  birthdaylem3  23283  rlimcnp  23295  efrlim  23299  cxplim  23301  cxp2lim  23306  cxploglim2  23308  divsqrtsumo1  23313  jensenlem2  23317  amgm  23320  logdifbnd  23323  harmonicbnd4  23340  fsumharmonic  23341  ftalem1  23346  ftalem5  23350  basellem1  23354  basellem8  23361  ppip1le  23435  ppiltx  23451  sqff1o  23456  chtublem  23486  chpub  23495  logfaclbnd  23497  logfacrlim  23499  logexprlim  23500  mersenne  23502  bcmono  23552  bcmax  23553  bposlem2  23560  bposlem5  23563  lgslem3  23573  lgsquadlem1  23629  lgsquadlem2  23630  2sqblem  23652  chebbnd1  23657  chtppilimlem1  23658  chto1ub  23661  chpchtlim  23664  chpo1ubb  23666  rplogsumlem1  23669  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlem1  23674  dchrisumlem2  23675  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0fno1  23696  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  rplogsum  23712  mudivsum  23715  mulogsumlem  23716  mulog2sumlem1  23719  mulog2sumlem2  23720  vmalogdivsum2  23723  2vmadivsumlem  23725  selberglem2  23731  selberg2b  23737  logdivbnd  23741  selberg3lem1  23742  selberg3lem2  23743  selberg4lem1  23745  pntrmax  23749  pntrsumo1  23750  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem2  23776  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemo  23792  pnt  23799  padicabv  23815  ostth2lem2  23819  ostth2lem3  23820  ostth3  23823  colperpexlem3  24106  mideulem2  24108  brbtwn2  24208  colinearalglem4  24212  nvmtri2  25575  nvabs  25576  nvge0  25577  nvlmle  25602  smcnlem  25607  nmblolbii  25714  blocnilem  25719  siii  25768  ubthlem2  25787  minvecolem3  25792  htthlem  25834  bcsiALT  26096  bcs3  26100  chscllem4  26558  0cnop  26898  0cnfn  26899  nmbdoplbi  26943  nmcoplbi  26947  nmophmi  26950  nmbdfnlbi  26968  nmcfnlbi  26971  nlelchi  26980  riesz1  26984  cnlnadjlem2  26987  nmopadjlei  27007  nmoptrii  27013  nmopcoi  27014  nmopcoadji  27020  unierri  27023  branmfn  27024  pjs14i  27129  hstle  27149  cdj3lem2b  27356  xlt2addrd  27578  eliccelico  27588  elicoelioo  27589  ltesubnnd  27612  archirngz  27733  archiabllem2c  27739  locfinref  27844  sqsscirc1  27890  tpr2rico  27894  esumcst  28071  measunl  28187  measiun  28189  eulerpartlemgc  28301  eulerpartlemb  28307  ballotlemsel1i  28451  ballotlemro  28461  sgnsub  28483  signsplypnf  28507  signsply0  28508  signsvtn  28541  signsvfnn  28543  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgambdd  28579  lgamcvg2  28597  erdsze2lem1  28647  sinccvglem  29038  divcnvlin  29118  iprodefisum  29124  faclimlem2  29169  nodense  29449  nobnddown  29461  supadd  30042  ltflcei  30043  opnmbllem0  30050  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  ibladdnclem  30071  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anc  30098  fnemeet1  30184  geomcau  30252  prdsbnd  30289  cntotbnd  30292  heiborlem4  30310  rrndstprj2  30327  rrncmslem  30328  rrnequiv  30331  iccbnd  30336  lzenom  30703  icodiamlt  30756  irrapxlem2  30759  irrapxlem3  30760  irrapxlem5  30762  pellexlem2  30766  pell14qrgt0  30795  pellfundlb  30820  pellfundex  30822  pellfund14  30834  rmspecsqrtnq  30842  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  congabseq  30912  acongrep  30918  acongeq  30921  jm2.26lem3  30943  jm2.27a  30947  jm2.27c  30949  hbtlem2  31073  dgraaub  31097  idomodle  31153  lcmledvds  31205  hashnzfzclim  31227  binomcxplemfrat  31256  binomcxplemnotnn0  31261  suprnmpt  31451  dstregt0  31463  lefldiveq  31482  fzisoeu  31500  upbdrech  31505  ssfiunibd  31509  fzdifsuc2  31512  divge1  31513  ioondisj2  31525  iccshift  31558  iooshift  31562  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fprodge1  31598  fprodle  31604  climrec  31609  climsuse  31614  mullimc  31622  mullimcf  31629  constlimc  31630  idlimc  31632  divcnvg  31633  limcperiod  31634  limcrecl  31635  lptioo2  31637  lptioo1  31638  islpcn  31645  lptre2pt  31646  limcleqr  31650  neglimc  31653  addlimc  31654  0ellimcdiv  31655  limclner  31657  sinaover2ne0  31668  cncfshift  31676  cncfperiod  31681  cncfioobdlem  31699  cncfioobd  31700  fperdvper  31715  dvdivbd  31720  dvbdfbdioolem1  31725  dvbdfbdioolem2  31726  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  dvnprodlem1  31743  itgiccshift  31779  itgperiod  31780  stoweidlem1  31783  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem16  31798  stoweidlem21  31803  stoweidlem25  31807  stoweidlem26  31808  stoweidlem36  31818  stoweidlem38  31820  stoweidlem41  31823  stoweidlem42  31824  stoweidlem45  31827  stoweidlem48  31830  stoweidlem52  31834  stoweidlem62  31844  wallispilem3  31849  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem12  31867  stirlinglem15  31870  dirkercncflem1  31885  fourierdlem10  31899  fourierdlem12  31901  fourierdlem15  31904  fourierdlem16  31905  fourierdlem19  31908  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem24  31913  fourierdlem30  31919  fourierdlem37  31926  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem52  31941  fourierdlem54  31943  fourierdlem60  31949  fourierdlem61  31950  fourierdlem63  31952  fourierdlem64  31953  fourierdlem68  31957  fourierdlem71  31960  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem77  31966  fourierdlem78  31967  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem87  31976  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  elaa2lem  32016  etransclem23  32040  etransclem28  32045  etransclem32  32049  etransclem35  32052  etransclem48  32065  pgrple2abl  32958  cvlcvr1  35064  cvrat3  35166  dalem25  35422  cdlema1N  35515  dalawlem3  35597  dalawlem4  35598  dalawlem5  35599  dalawlem6  35600  dalawlem7  35601  dalawlem9  35603  dalawlem11  35605  dalawlem12  35606  lhp2lt  35725  lhpmcvr  35747  4atexlemcnd  35796  lautj  35817  trlle  35909  trlval3  35912  trlval4  35913  cdleme0moN  35950  cdleme13  35997  cdleme15  36003  cdleme19b  36030  cdleme20e  36039  cdleme20j  36044  cdleme22e  36070  cdleme22eALTN  36071  cdleme26fALTN  36088  cdleme26f  36089  cdleme27N  36095  cdleme41sn3a  36159  cdleme46fsvlpq  36231  cdlemeg46vrg  36253  cdlemg4  36343  cdlemg7N  36352  cdlemg9a  36358  cdlemg11b  36368  cdlemg12a  36369  trljco  36466  tendoidcl  36495  tendococl  36498  tendopltp  36506  tendo0tp  36515  tendoicl  36522  cdlemi2  36545  cdlemk5a  36561  cdlemk5  36562  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk12u  36598  cdlemk37  36640  cdlemk39s-id  36666  cdlemk49  36677  cdlemk39u1  36693  cdlemk39u  36694  dian0  36766  cdlemm10N  36845  cdlemn2  36922  cdlemn10  36933  dihord1  36945  dihord10  36950  dihmeetlem4preN  37033  dihmeetlem18N  37051  dihmeetlem20N  37053  dihjatc  37144  mapdcnvatN  37393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator