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

Theorem eqbrtrd 4826
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 4814 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 247 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805
This theorem is referenced by:  eqbrtrrd  4828  somin2  5689  en1b  8189  domunsncan  8225  fodomfi  8404  hartogslem1  8612  wemaplem2  8617  infdifsn  8727  carddomi2  8986  cdaun  9186  cda1dif  9190  mapcdaen  9198  cdaxpdom  9203  cdafi  9204  cdainf  9206  carden  9565  alephsuc3  9594  fpwwe2lem6  9649  fpwwe2lem7  9650  inar1  9789  rankcf  9791  lesub3d  10837  lbinfle  11170  supadd  11183  supmul  11187  rpnnen1lem3  12009  rpnnen1lem3OLD  12015  divge1  12091  xrmin1  12201  xrmin2  12202  ifle  12221  qbtwnxr  12224  xltnegi  12240  xleadd1a  12276  xlt2add  12283  xlemul1a  12311  xov1plusxeqvd  12511  ubmelm1fzo  12758  flflp1  12802  ceim1l  12840  ceilm1lt  12841  ceille  12843  quoremz  12848  quoremnn0ALT  12850  modlt  12873  modeqmodmin  12934  addmodlteq  12939  seqf1olem1  13034  bernneq  13184  discr  13195  faclbnd2  13272  faclbnd4lem3  13276  hashun2  13364  hashfun  13416  ccatsymb  13554  ccatrn  13561  sqrlem6  14187  sqrlem7  14188  rddif  14279  amgm2  14308  icodiamlt  14373  climconst  14473  rlimconst  14474  serclim0  14507  rlimcn1  14518  mulcn2  14525  reccn2  14526  o1mul  14544  o1rlimmul  14548  iserex  14586  climlec2  14588  iserge0  14590  climcau  14600  caucvgrlem  14602  caucvgr  14605  iseraltlem2  14612  iseraltlem3  14613  iseralt  14614  fsumabs  14732  o1fsum  14744  iserabs  14746  climfsum  14751  isumless  14776  climcndslem2  14781  divrcnv  14783  flo1  14785  supcvg  14787  georeclim  14802  geomulcvg  14806  cvgrat  14814  mertenslem1  14815  prodfclim1  14824  fprodge1  14925  fprodle  14926  efcvgfsum  15015  eftlub  15038  eflegeo  15050  tanhlt1  15089  tanhbnd  15090  ef01bndlem  15113  sin01bnd  15114  cos01bnd  15115  cos01gt0  15120  ruclem2  15160  ruclem3  15161  ruclem9  15166  ruclem11  15168  ruclem12  15169  bitsfzolem  15358  bitsfzo  15359  bitsinv1lem  15365  sadcaddlem  15381  mulgcd  15467  eucalglt  15500  lcmledvds  15514  lcmfledvds  15547  mulgcddvds  15571  coprmproddvdslem  15578  prmind2  15600  isprm5  15621  divdenle  15659  nonsq  15669  pythagtriplem4  15726  pclem  15745  pcpremul  15750  pczdvds  15769  pcprmpw2  15788  qexpz  15807  prmreclem4  15825  prmreclem5  15826  4sqlem10  15853  ramtub  15918  ramub2  15920  prmodvdslcmf  15953  prmgaplem8  15964  natpropd  16837  catciso  16958  p0le  17244  acsdomd  17382  qusgrp  17850  f1otrspeq  18067  pmtrfrn  18078  pmtrfconj  18086  symggen  18090  psgnunilem4  18117  oddvds2  18183  odcau  18219  pgpfi  18220  pgpssslw  18229  sylow3lem4  18245  efgred2  18366  frgp0  18373  odadd2  18452  oddvdssubg  18458  ablfac1c  18670  ablfac1eu  18672  pgpfaclem3  18682  isabvd  19022  abvsubtri  19037  mplsubrg  19642  coe1sfi  19785  cyggic  20123  mp2pm2mplem5  20817  en2top  20991  1stcrest  21458  2ndcrest  21459  hausmapdom  21505  ufilen  21935  xmetrtri2  22362  prdsxmetlem  22374  bl2in  22406  xblcntrps  22416  xblcntr  22417  ssblps  22428  ssbl  22429  blssps  22430  blss  22431  blcld  22511  methaus  22526  metustexhalf  22562  nmtri2  22632  tngngp3  22661  nrginvrcnlem  22696  nrginvrcn  22697  nmoi  22733  nmo0  22740  nmoid  22747  blcvx  22802  reperflem  22822  reconnlem2  22831  metdcnlem  22840  metdscn  22860  metnrmlem3  22865  mulc1cncf  22909  iccpnfhmeo  22945  cnheiborlem  22954  cnheibor  22955  lebnumii  22966  pcopt  23022  pcopt2  23023  pcoass  23024  nmoleub2lem  23114  nmoleub2lem3  23115  nmoleub2lem2  23116  ipcau2  23233  tchcphlem1  23234  nglmle  23300  trirn  23383  rrxdstprj1  23392  minveclem3  23400  ivthlem2  23421  ivthlem3  23422  ivth2  23424  ovollb  23447  ovolsslem  23452  ovollb2lem  23456  ovolctb  23458  ovoliunlem1  23470  ovolsca  23483  ovolicc1  23484  ovolicc2lem4  23488  nulmbl  23503  ioombl1lem4  23529  uniioovol  23547  uniioombllem3a  23552  uniioombllem4  23554  opnmbllem  23569  volcn  23574  volivth  23575  i1fadd  23661  i1fmul  23662  mbfi1fseqlem4  23684  mbfi1fseqlem5  23685  mbfi1fseqlem6  23686  itg2const2  23707  itg2seq  23708  itg2uba  23709  itg2split  23715  itg2monolem1  23716  itg2monolem3  23718  itg2i1fseq2  23722  itg2addlem  23724  itg2gt0  23726  itg2cnlem1  23727  itg2cnlem2  23728  itgless  23782  ibladdlem  23785  bddmulibl  23804  dveflem  23941  dvferm1lem  23946  dvferm2lem  23948  dvlip  23955  dvlipcn  23956  dvlip2  23957  dvle  23969  dvivthlem1  23970  lhop1lem  23975  dvcvx  23982  dvfsumabs  23985  dvfsumlem2  23989  dvfsumlem4  23991  dvfsumrlim2  23994  dvfsum2  23996  ftc1a  23999  ftc1lem4  24001  ftc1lem5  24002  deg1sub  24067  ply1divex  24095  deg1submon1p  24111  r1pdeglt  24117  dvdsq1p  24119  fta1glem2  24125  fta1g  24126  plyeq0lem  24165  dgrlt  24221  fta1lem  24261  aalioulem2  24287  aalioulem3  24288  aalioulem4  24289  aaliou3lem2  24297  aaliou3lem9  24304  taylply2  24321  ulmbdd  24351  ulmdvlem1  24353  mtest  24357  mtestbdd  24358  radcnvlem1  24366  radcnvle  24373  pserulm  24375  psercn  24379  pserdvlem2  24381  abelthlem2  24385  abelthlem5  24388  abelthlem7  24391  abelthlem8  24392  abelthlem9  24393  reeff1olem  24399  tangtx  24456  tanord  24483  efif1olem4  24490  logrnaddcl  24520  logcj  24551  logimul  24559  logneg2  24560  logdivlti  24565  divlogrlim  24580  logcnlem3  24589  logcnlem4  24590  efopn  24603  logtayllem  24604  logtayl  24605  cxpcn3lem  24687  cxpaddle  24692  abscxpbnd  24693  asinlem3  24797  asinneg  24812  asinsin  24818  atanlogaddlem  24839  atantan  24849  bndatandm  24855  atans2  24857  atantayl  24863  atantayl2  24864  atantayl3  24865  leibpi  24868  birthdaylem3  24879  rlimcnp  24891  efrlim  24895  cxplim  24897  cxp2lim  24902  cxploglim2  24904  divsqrtsumo1  24909  jensenlem2  24913  amgm  24916  logdifbnd  24919  harmonicbnd4  24936  fsumharmonic  24937  lgamgulmlem2  24955  lgamgulmlem3  24956  lgamgulmlem5  24958  lgambdd  24962  lgamcvg2  24980  ftalem1  24998  ftalem5  25002  basellem1  25006  basellem8  25013  ppip1le  25086  ppiltx  25102  sqff1o  25107  chtublem  25135  chpub  25144  logfaclbnd  25146  logfacrlim  25148  logexprlim  25149  mersenne  25151  bcmono  25201  bcmax  25202  bposlem2  25209  bposlem5  25212  lgslem3  25223  gausslemma2dlem1a  25289  lgsquadlem1  25304  lgsquadlem2  25305  2lgslem1c  25317  2sqblem  25355  chebbnd1  25360  chtppilimlem1  25361  chto1ub  25364  chpchtlim  25367  chpo1ubb  25369  rplogsumlem1  25372  rplogsumlem2  25373  rpvmasumlem  25375  dchrisumlem1  25377  dchrisumlem2  25378  dchrmusum2  25382  dchrvmasumlem2  25386  dchrvmasumlem3  25387  dchrvmasumiflem1  25389  dchrisum0flblem1  25396  dchrisum0fno1  25399  dchrisum0lem1b  25403  dchrisum0lem1  25404  dchrisum0lem2a  25405  dchrisum0lem2  25406  rplogsum  25415  mudivsum  25418  mulogsumlem  25419  mulog2sumlem1  25422  mulog2sumlem2  25423  vmalogdivsum2  25426  2vmadivsumlem  25428  selberglem2  25434  selberg2b  25440  logdivbnd  25444  selberg3lem1  25445  selberg3lem2  25446  selberg4lem1  25448  pntrmax  25452  pntrsumo1  25453  pntrlog2bndlem1  25465  pntrlog2bndlem2  25466  pntrlog2bndlem3  25467  pntrlog2bndlem4  25468  pntrlog2bndlem5  25469  pntrlog2bnd  25472  pntpbnd1a  25473  pntpbnd2  25475  pntibndlem2  25479  pntlemb  25485  pntlemg  25486  pntlemh  25487  pntlemr  25490  pntlemj  25491  pntlemf  25493  pntlemo  25495  pnt  25502  padicabv  25518  ostth2lem2  25522  ostth2lem3  25523  ostth3  25526  colperpexlem3  25823  mideulem2  25825  lnperpex  25894  trgcopy  25895  iscgra1  25901  brbtwn2  25984  colinearalglem4  25988  subupgr  26378  crctcshwlkn0lem1  26913  nvabs  27836  nvge0  27837  smcnlem  27861  nmblolbii  27963  blocnilem  27968  siii  28017  ubthlem2  28036  minvecolem3  28041  htthlem  28083  bcsiALT  28345  bcs3  28349  chscllem4  28808  0cnop  29147  0cnfn  29148  nmbdoplbi  29192  nmcoplbi  29196  nmophmi  29199  nmbdfnlbi  29217  nmcfnlbi  29220  nlelchi  29229  riesz1  29233  cnlnadjlem2  29236  nmopadjlei  29256  nmoptrii  29262  nmopcoi  29263  nmopcoadji  29269  unierri  29272  branmfn  29273  pjs14i  29378  hstle  29398  cdj3lem2b  29605  xlt2addrd  29832  eliccelico  29848  elicoelioo  29849  ltesubnnd  29877  archirngz  30052  archiabllem2c  30058  madjusmdetlem2  30203  locfinref  30217  sqsscirc1  30263  tpr2rico  30267  esumcst  30434  esumgect  30461  esum2d  30464  measunl  30588  measiun  30590  omssubaddlem  30670  omssubadd  30671  carsgsigalem  30686  carsgclctunlem2  30690  pmeasmono  30695  eulerpartlemgc  30733  eulerpartlemb  30739  ballotlemsel1i  30883  ballotlemro  30893  sgnsub  30915  signsplypnf  30936  signsply0  30937  signsvtn  30970  signsvfnn  30972  hgt750lemd  31035  logdivsqrle  31037  erdsze2lem1  31492  sinccvglem  31873  divcnvlin  31925  iprodefisum  31934  faclimlem2  31937  nosep1o  32138  nodense  32148  fnemeet1  32667  dnibndlem10  32783  dnibndlem11  32784  dnibnd  32787  knoppcnlem4  32792  knoppcnlem6  32794  unblimceq0lem  32803  unblimceq0  32804  unbdqndv2lem1  32806  unbdqndv2lem2  32807  knoppndvlem11  32819  knoppndvlem12  32820  knoppndvlem14  32822  knoppndvlem15  32823  knoppndvlem17  32825  knoppndvlem18  32826  knoppndvlem19  32827  knoppndvlem21  32829  ltflcei  33710  ptrecube  33722  poimirlem16  33738  poimirlem17  33739  poimirlem29  33751  broucube  33756  opnmbllem0  33758  mblfinlem2  33760  mblfinlem3  33761  ismblfin  33763  itg2addnclem  33774  itg2addnclem2  33775  itg2addnclem3  33776  itg2addnc  33777  ibladdnclem  33779  ftc1cnnclem  33796  ftc1cnnc  33797  ftc1anc  33806  geomcau  33868  prdsbnd  33905  cntotbnd  33908  heiborlem4  33926  rrndstprj2  33943  rrncmslem  33944  rrnequiv  33947  iccbnd  33952  cvlcvr1  35129  cvrat3  35231  dalem25  35487  cdlema1N  35580  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  lhp2lt  35790  lhpmcvr  35812  4atexlemcnd  35861  lautj  35882  trlle  35974  trlval3  35977  trlval4  35978  cdleme0moN  36015  cdleme13  36062  cdleme15  36068  cdleme19b  36094  cdleme20e  36103  cdleme20j  36108  cdleme22e  36134  cdleme22eALTN  36135  cdleme26fALTN  36152  cdleme26f  36153  cdleme27N  36159  cdleme41sn3a  36223  cdleme46fsvlpq  36295  cdlemeg46vrg  36317  cdlemg4  36407  cdlemg7N  36416  cdlemg9a  36422  cdlemg11b  36432  cdlemg12a  36433  trljco  36530  tendoidcl  36559  tendococl  36562  tendopltp  36570  tendo0tp  36579  tendoicl  36586  cdlemi2  36609  cdlemk5a  36625  cdlemk5  36626  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk12u  36662  cdlemk37  36704  cdlemk39s-id  36730  cdlemk49  36741  cdlemk39u1  36757  cdlemk39u  36758  dian0  36830  cdlemm10N  36909  cdlemn2  36986  cdlemn10  36997  dihord1  37009  dihord10  37014  dihmeetlem4preN  37097  dihmeetlem18N  37115  dihmeetlem20N  37117  dihjatc  37208  mapdcnvatN  37457  lzenom  37835  irrapxlem2  37889  irrapxlem3  37890  irrapxlem5  37892  pellexlem2  37896  pell14qrgt0  37925  pellfundlb  37950  pellfundex  37952  pellfund14  37964  rmspecsqrtnq  37972  rmspecsqrtnqOLD  37973  jm2.24nn  38028  jm2.17a  38029  jm2.17b  38030  congabseq  38043  acongrep  38049  acongeq  38052  jm2.26lem3  38070  jm2.27a  38074  jm2.27c  38076  hbtlem2  38196  dgraaub  38220  idomodle  38276  relexpxpmin  38511  frege102d  38548  hashnzfzclim  39023  binomcxplemfrat  39052  binomcxplemnotnn0  39057  suprnmpt  39854  mpct  39892  rnmptbddlem  39954  dstregt0  39992  lefldiveq  40004  fzisoeu  40013  upbdrech  40018  ssfiunibd  40022  fzdifsuc2  40023  xadd0ge  40034  supxrgere  40047  supxrge  40052  suplesup  40053  xrlexaddrp  40066  infxrunb2  40082  infleinflem2  40085  reclt0d  40105  infrpgernmpt  40193  ioondisj2  40217  iccshift  40247  iooshift  40251  fmul01  40315  fmul01lt1lem1  40319  fmul01lt1lem2  40320  climrec  40338  climsuse  40343  mullimc  40351  mullimcf  40358  constlimc  40359  idlimc  40361  divcnvg  40362  limcperiod  40363  limcrecl  40364  lptioo2  40366  lptioo1  40367  islpcn  40374  lptre2pt  40375  limcleqr  40379  neglimc  40382  addlimc  40383  0ellimcdiv  40384  limclner  40386  climleltrp  40411  limsuplesup  40434  limsupmnflem  40455  supcnvlimsupmpt  40476  0cnv  40477  xlimconst  40554  sinaover2ne0  40582  cncfshift  40590  cncfperiod  40595  cncfioobdlem  40612  cncfioobd  40613  fperdvper  40636  dvdivbd  40641  dvbdfbdioolem1  40646  dvbdfbdioolem2  40647  ioodvbdlimc1lem1  40649  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnmul  40661  dvnprodlem1  40664  itgiccshift  40699  itgperiod  40700  ismbl3  40706  ovolsplit  40708  stoweidlem1  40721  stoweidlem11  40731  stoweidlem13  40733  stoweidlem14  40734  stoweidlem16  40736  stoweidlem21  40741  stoweidlem25  40745  stoweidlem26  40746  stoweidlem36  40756  stoweidlem38  40758  stoweidlem41  40761  stoweidlem42  40762  stoweidlem45  40765  stoweidlem48  40768  stoweidlem52  40772  stoweidlem62  40782  wallispilem3  40787  stirlinglem5  40798  stirlinglem6  40799  stirlinglem7  40800  stirlinglem10  40803  stirlinglem12  40805  stirlinglem15  40808  dirkercncflem1  40823  fourierdlem10  40837  fourierdlem12  40839  fourierdlem15  40842  fourierdlem16  40843  fourierdlem19  40846  fourierdlem20  40847  fourierdlem21  40848  fourierdlem22  40849  fourierdlem24  40851  fourierdlem30  40857  fourierdlem37  40864  fourierdlem39  40866  fourierdlem40  40867  fourierdlem41  40868  fourierdlem42  40869  fourierdlem47  40873  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem52  40878  fourierdlem54  40880  fourierdlem60  40886  fourierdlem61  40887  fourierdlem63  40889  fourierdlem64  40890  fourierdlem68  40894  fourierdlem71  40897  fourierdlem72  40898  fourierdlem73  40899  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem77  40903  fourierdlem78  40904  fourierdlem79  40905  fourierdlem81  40907  fourierdlem82  40908  fourierdlem83  40909  fourierdlem84  40910  fourierdlem87  40913  fourierdlem92  40918  fourierdlem93  40919  fourierdlem94  40920  fourierdlem101  40927  fourierdlem102  40928  fourierdlem103  40929  fourierdlem104  40930  fourierdlem111  40937  fourierdlem112  40938  fourierdlem113  40939  fourierdlem114  40940  sqwvfoura  40948  sqwvfourb  40949  fouriersw  40951  elaa2lem  40953  etransclem23  40977  etransclem28  40982  etransclem32  40986  etransclem35  40989  etransclem48  41002  qndenserrnbllem  41017  rrnprjdstle  41024  ioorrnopnlem  41027  ioorrnopnxrlem  41029  salexct  41055  sge0fsum  41107  sge0supre  41109  sge0rnbnd  41113  sge0lefi  41118  sge0lessmpt  41119  sge0ltfirp  41120  sge0prle  41121  sge0resrnlem  41123  sge0le  41127  sge0split  41129  sge0iunmptlemre  41135  sge0iunmpt  41138  sge0isum  41147  sge0xaddlem1  41153  sge0xaddlem2  41154  sge0xadd  41155  sge0reuz  41167  sge0reuzb  41168  meaunle  41184  meaiunlelem  41188  voliunsge0lem  41192  meaiuninc  41201  meaiininclem  41206  omeunle  41236  omeiunle  41237  omelesplit  41238  omeiunltfirp  41239  carageniuncllem2  41242  caratheodorylem2  41247  caragencmpl  41255  ovnlecvr  41278  ovncvrrp  41284  ovnsubaddlem1  41290  ovnsubadd  41292  hoidmv1lelem1  41311  hoidmv1lelem2  41312  hoidmv1le  41314  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem5  41319  hoidmvle  41320  ovnhoilem1  41321  ovnlecvr2  41330  ovncvr2  41331  hoiqssbllem2  41343  hspmbllem2  41347  hspmbllem3  41348  ovnsplit  41368  ovolval5lem1  41372  vonioolem1  41400  vonioolem2  41401  vonicclem1  41403  vonicclem2  41404  pimconstlt1  41421  smflimlem2  41486  smflimlem4  41488  smfmullem1  41504  smfsuplem1  41523  smflimsuplem4  41535  smflimsuplem5  41536  iccpartltu  41871  iccpartleu  41874  pgrple2abl  42656  difmodm1lt  42827  nnpw2blen  42884  dignn0flhalflem1  42919
  Copyright terms: Public domain W3C validator