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

Theorem eqbrtrd 4819
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 4807 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 248 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1634   class class class wbr 4797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798
This theorem is referenced by:  eqbrtrrd  4821  somin2  5683  en1b  8198  domunsncan  8237  fodomfi  8416  hartogslem1  8624  wemaplem2  8629  infdifsn  8739  carddomi2  9017  cdaun  9217  cda1dif  9221  mapcdaen  9229  cdaxpdom  9234  cdafi  9235  cdainf  9237  carden  9596  alephsuc3  9625  fpwwe2lem6  9680  fpwwe2lem7  9681  inar1  9820  rankcf  9822  lesub3d  10868  lbinfle  11201  supadd  11214  supmul  11218  rpnnen1lem3  12041  divge1  12118  xrmin1  12232  xrmin2  12233  ifle  12252  qbtwnxr  12255  xltnegi  12271  xleadd1a  12307  xlt2add  12314  xlemul1a  12342  xov1plusxeqvd  12547  ubmelm1fzo  12794  flflp1  12838  ceim1l  12876  ceilm1lt  12877  ceille  12879  quoremz  12884  quoremnn0ALT  12886  modlt  12909  modeqmodmin  12970  addmodlteq  12975  seqf1olem1  13069  bernneq  13219  discr  13230  faclbnd2  13304  faclbnd4lem3  13308  hashun2  13396  hashfun  13448  ccatsymb  13586  ccatrn  13593  sqrlem6  14218  sqrlem7  14219  rddif  14310  amgm2  14339  icodiamlt  14404  climconst  14504  rlimconst  14505  serclim0  14538  rlimcn1  14549  mulcn2  14556  reccn2  14557  o1mul  14575  o1rlimmul  14579  iserex  14617  climlec2  14619  iserge0  14621  climcau  14631  caucvgrlem  14633  caucvgr  14636  iseraltlem2  14643  iseraltlem3  14644  iseralt  14645  fsumabs  14762  o1fsum  14774  iserabs  14776  climfsum  14781  isumless  14806  climcndslem2  14811  divrcnv  14813  flo1  14815  supcvg  14817  georeclim  14832  geomulcvg  14836  cvgrat  14844  mertenslem1  14845  prodfclim1  14854  fprodge1  14954  fprodle  14955  efcvgfsum  15044  eftlub  15067  eflegeo  15079  tanhlt1  15118  tanhbnd  15119  ef01bndlem  15142  sin01bnd  15143  cos01bnd  15144  cos01gt0  15149  ruclem2  15189  ruclem3  15190  ruclem9  15195  ruclem11  15197  ruclem12  15198  bitsfzolem  15385  bitsfzo  15386  bitsinv1lem  15392  sadcaddlem  15408  mulgcd  15494  eucalglt  15527  lcmledvds  15541  lcmfledvds  15574  mulgcddvds  15597  coprmproddvdslem  15604  prmind2  15626  isprm5  15646  divdenle  15684  nonsq  15694  pythagtriplem4  15751  pclem  15770  pcpremul  15775  pczdvds  15794  pcprmpw2  15813  qexpz  15832  prmreclem4  15850  prmreclem5  15851  4sqlem10  15878  ramtub  15943  ramub2  15945  prmodvdslcmf  15978  prmgaplem8  15989  natpropd  16863  catciso  16984  p0le  17271  acsdomd  17409  qusgrp  17877  f1otrspeq  18094  pmtrfrn  18105  pmtrfconj  18113  symggen  18117  psgnunilem4  18144  oddvds2  18210  odcau  18246  pgpfi  18247  pgpssslw  18256  sylow3lem4  18272  efgred2  18393  frgp0  18400  odadd2  18479  oddvdssubg  18485  ablfac1c  18698  ablfac1eu  18700  pgpfaclem3  18710  isabvd  19050  abvsubtri  19065  mplsubrg  19675  coe1sfi  19818  cyggic  20156  mp2pm2mplem5  20855  en2top  21030  1stcrest  21497  2ndcrest  21498  hausmapdom  21544  ufilen  21974  xmetrtri2  22401  prdsxmetlem  22413  bl2in  22445  xblcntrps  22455  xblcntr  22456  ssblps  22467  ssbl  22468  blssps  22469  blss  22470  blcld  22550  methaus  22565  metustexhalf  22601  nmtri2  22671  tngngp3  22700  nrginvrcnlem  22735  nrginvrcn  22736  nmoi  22772  nmo0  22779  nmoid  22786  blcvx  22841  reperflem  22861  reconnlem2  22870  metdcnlem  22879  metdscn  22899  metnrmlem3  22904  mulc1cncf  22948  iccpnfhmeo  22984  cnheiborlem  22993  cnheibor  22994  lebnumii  23005  pcopt  23061  pcopt2  23062  pcoass  23063  nmoleub2lem  23153  nmoleub2lem3  23154  nmoleub2lem2  23155  ipcau2  23272  tchcphlem1  23273  nglmle  23339  trirn  23422  rrxdstprj1  23431  minveclem3  23439  ivthlem2  23460  ivthlem3  23461  ivth2  23463  ovollb  23487  ovolsslem  23492  ovollb2lem  23496  ovolctb  23498  ovoliunlem1  23510  ovolsca  23523  ovolicc1  23524  ovolicc2lem4  23528  nulmbl  23543  ioombl1lem4  23569  uniioovol  23587  uniioombllem3a  23592  uniioombllem4  23594  opnmbllem  23609  volcn  23614  volivth  23615  i1fadd  23703  i1fmul  23704  mbfi1fseqlem4  23726  mbfi1fseqlem5  23727  mbfi1fseqlem6  23728  itg2const2  23749  itg2seq  23750  itg2uba  23751  itg2split  23757  itg2monolem1  23758  itg2monolem3  23760  itg2i1fseq2  23764  itg2addlem  23766  itg2gt0  23768  itg2cnlem1  23769  itg2cnlem2  23770  itgless  23824  ibladdlem  23827  bddmulibl  23846  dveflem  23983  dvferm1lem  23988  dvferm2lem  23990  dvlip  23997  dvlipcn  23998  dvlip2  23999  dvle  24011  dvivthlem1  24012  lhop1lem  24017  dvcvx  24024  dvfsumabs  24027  dvfsumlem2  24031  dvfsumlem4  24033  dvfsumrlim2  24036  dvfsum2  24038  ftc1a  24041  ftc1lem4  24043  ftc1lem5  24044  deg1sub  24109  ply1divex  24137  deg1submon1p  24153  r1pdeglt  24159  dvdsq1p  24161  fta1glem2  24167  fta1g  24168  plyeq0lem  24207  dgrlt  24263  fta1lem  24303  aalioulem2  24329  aalioulem3  24330  aalioulem4  24331  aaliou3lem2  24339  aaliou3lem9  24346  taylply2  24363  ulmbdd  24393  ulmdvlem1  24395  mtest  24399  mtestbdd  24400  radcnvlem1  24408  radcnvle  24415  pserulm  24417  psercn  24421  pserdvlem2  24423  abelthlem2  24427  abelthlem5  24430  abelthlem7  24433  abelthlem8  24434  abelthlem9  24435  reeff1olem  24441  tangtx  24499  tanord  24526  efif1olem4  24533  logrnaddcl  24563  logcj  24594  logimul  24602  logneg2  24603  logdivlti  24608  divlogrlim  24623  logcnlem3  24632  logcnlem4  24633  efopn  24646  logtayllem  24647  logtayl  24648  cxpcn3lem  24730  cxpaddle  24735  abscxpbnd  24736  asinlem3  24840  asinneg  24855  asinsin  24861  atanlogaddlem  24882  atantan  24892  bndatandm  24898  atans2  24900  atantayl  24906  atantayl2  24907  atantayl3  24908  leibpi  24911  birthdaylem3  24922  rlimcnp  24934  efrlim  24938  cxplim  24940  cxp2lim  24945  cxploglim2  24947  divsqrtsumo1  24952  jensenlem2  24956  amgm  24959  logdifbnd  24962  harmonicbnd4  24979  fsumharmonic  24980  lgamgulmlem2  24998  lgamgulmlem3  24999  lgamgulmlem5  25001  lgambdd  25005  lgamcvg2  25023  ftalem1  25041  ftalem5  25045  basellem1  25049  basellem8  25056  ppip1le  25129  ppiltx  25145  sqff1o  25150  chtublem  25178  chpub  25187  logfaclbnd  25189  logfacrlim  25191  logexprlim  25192  mersenne  25194  bcmono  25244  bcmax  25245  bposlem2  25252  bposlem5  25255  lgslem3  25266  gausslemma2dlem1a  25332  lgsquadlem1  25347  lgsquadlem2  25348  2lgslem1c  25360  2sqblem  25398  chebbnd1  25403  chtppilimlem1  25404  chto1ub  25407  chpchtlim  25410  chpo1ubb  25412  rplogsumlem1  25415  rplogsumlem2  25416  rpvmasumlem  25418  dchrisumlem1  25420  dchrisumlem2  25421  dchrmusum2  25425  dchrvmasumlem2  25429  dchrvmasumlem3  25430  dchrvmasumiflem1  25432  dchrisum0flblem1  25439  dchrisum0fno1  25442  dchrisum0lem1b  25446  dchrisum0lem1  25447  dchrisum0lem2a  25448  dchrisum0lem2  25449  rplogsum  25458  mudivsum  25461  mulogsumlem  25462  mulog2sumlem1  25465  mulog2sumlem2  25466  vmalogdivsum2  25469  2vmadivsumlem  25471  selberglem2  25477  selberg2b  25483  logdivbnd  25487  selberg3lem1  25488  selberg3lem2  25489  selberg4lem1  25491  pntrmax  25495  pntrsumo1  25496  pntrlog2bndlem1  25508  pntrlog2bndlem2  25509  pntrlog2bndlem3  25510  pntrlog2bndlem4  25511  pntrlog2bndlem5  25512  pntrlog2bnd  25515  pntpbnd1a  25516  pntpbnd2  25518  pntibndlem2  25522  pntlemb  25528  pntlemg  25529  pntlemh  25530  pntlemr  25533  pntlemj  25534  pntlemf  25536  pntlemo  25538  pnt  25545  padicabv  25561  ostth2lem2  25565  ostth2lem3  25566  ostth3  25569  colperpexlem3  25866  mideulem2  25868  lnperpex  25937  trgcopy  25938  iscgra1  25944  brbtwn2  26027  colinearalglem4  26031  subupgr  26423  crctcshwlkn0lem1  26959  nvabs  27884  nvge0  27885  smcnlem  27909  nmblolbii  28011  blocnilem  28016  siii  28065  ubthlem2  28084  minvecolem3  28089  htthlem  28131  bcsiALT  28393  bcs3  28397  chscllem4  28856  0cnop  29195  0cnfn  29196  nmbdoplbi  29240  nmcoplbi  29244  nmophmi  29247  nmbdfnlbi  29265  nmcfnlbi  29268  nlelchi  29277  riesz1  29281  cnlnadjlem2  29284  nmopadjlei  29304  nmoptrii  29310  nmopcoi  29311  nmopcoadji  29317  unierri  29320  branmfn  29321  pjs14i  29426  hstle  29446  cdj3lem2b  29653  xlt2addrd  29880  eliccelico  29896  elicoelioo  29897  ltesubnnd  29925  archirngz  30100  archiabllem2c  30106  madjusmdetlem2  30251  locfinref  30265  sqsscirc1  30311  tpr2rico  30315  esumcst  30482  esumgect  30509  esum2d  30512  measunl  30636  measiun  30638  omssubaddlem  30718  omssubadd  30719  carsgsigalem  30734  carsgclctunlem2  30738  pmeasmono  30743  eulerpartlemgc  30781  eulerpartlemb  30787  ballotlemsel1i  30931  ballotlemro  30941  sgnsub  30963  signsplypnf  30984  signsply0  30985  signsvtn  31018  signsvfnn  31020  hgt750lemd  31083  logdivsqrle  31085  erdsze2lem1  31540  sinccvglem  31921  divcnvlin  31973  iprodefisum  31982  faclimlem2  31985  nosep1o  32186  nodense  32196  fnemeet1  32715  dnibndlem10  32831  dnibndlem11  32832  dnibnd  32835  knoppcnlem4  32840  knoppcnlem6  32842  unblimceq0lem  32851  unblimceq0  32852  unbdqndv2lem1  32854  unbdqndv2lem2  32855  knoppndvlem11  32867  knoppndvlem12  32868  knoppndvlem14  32870  knoppndvlem15  32871  knoppndvlem17  32873  knoppndvlem18  32874  knoppndvlem19  32875  knoppndvlem21  32877  ltflcei  33747  ptrecube  33759  poimirlem16  33775  poimirlem17  33776  poimirlem29  33788  broucube  33793  opnmbllem0  33795  mblfinlem2  33797  mblfinlem3  33798  ismblfin  33800  itg2addnclem  33810  itg2addnclem2  33811  itg2addnclem3  33812  itg2addnc  33813  ibladdnclem  33815  ftc1cnnclem  33832  ftc1cnnc  33833  ftc1anc  33842  geomcau  33903  prdsbnd  33940  cntotbnd  33943  heiborlem4  33961  rrndstprj2  33978  rrncmslem  33979  rrnequiv  33982  iccbnd  33987  cvlcvr1  35163  cvrat3  35266  dalem25  35522  cdlema1N  35615  dalawlem3  35697  dalawlem4  35698  dalawlem5  35699  dalawlem6  35700  dalawlem7  35701  dalawlem9  35703  dalawlem11  35705  dalawlem12  35706  lhp2lt  35825  lhpmcvr  35847  4atexlemcnd  35896  lautj  35917  trlle  36009  trlval3  36012  trlval4  36013  cdleme0moN  36050  cdleme13  36097  cdleme15  36103  cdleme19b  36129  cdleme20e  36138  cdleme20j  36143  cdleme22e  36169  cdleme22eALTN  36170  cdleme26fALTN  36187  cdleme26f  36188  cdleme27N  36194  cdleme41sn3a  36258  cdleme46fsvlpq  36330  cdlemeg46vrg  36352  cdlemg4  36442  cdlemg7N  36451  cdlemg9a  36457  cdlemg11b  36467  cdlemg12a  36468  trljco  36565  tendoidcl  36594  tendococl  36597  tendopltp  36605  tendo0tp  36614  tendoicl  36621  cdlemi2  36644  cdlemk5a  36660  cdlemk5  36661  cdlemk12  36675  cdlemkole  36678  cdlemk14  36679  cdlemk12u  36697  cdlemk37  36739  cdlemk39s-id  36765  cdlemk49  36776  cdlemk39u1  36792  cdlemk39u  36793  dian0  36864  cdlemm10N  36943  cdlemn2  37020  cdlemn10  37031  dihord1  37043  dihord10  37048  dihmeetlem4preN  37131  dihmeetlem18N  37149  dihmeetlem20N  37151  dihjatc  37242  mapdcnvatN  37491  lzenom  37874  irrapxlem2  37928  irrapxlem3  37929  irrapxlem5  37931  pellexlem2  37935  pell14qrgt0  37964  pellfundlb  37989  pellfundex  37991  pellfund14  38003  rmspecsqrtnq  38011  rmspecsqrtnqOLD  38012  jm2.24nn  38067  jm2.17a  38068  jm2.17b  38069  congabseq  38082  acongrep  38088  acongeq  38091  jm2.26lem3  38109  jm2.27a  38113  jm2.27c  38115  hbtlem2  38235  dgraaub  38259  idomodle  38315  relexpxpmin  38549  frege102d  38586  hashnzfzclim  39061  binomcxplemfrat  39090  binomcxplemnotnn0  39095  suprnmpt  39886  mpct  39922  rnmptbddlem  39982  dstregt0  40019  lefldiveq  40031  fzisoeu  40039  upbdrech  40044  ssfiunibd  40048  fzdifsuc2  40049  xadd0ge  40060  supxrgere  40073  supxrge  40078  suplesup  40079  xrlexaddrp  40092  infxrunb2  40108  infleinflem2  40111  reclt0d  40131  infrpgernmpt  40218  ioondisj2  40242  iccshift  40269  iooshift  40273  fmul01  40336  fmul01lt1lem1  40340  fmul01lt1lem2  40341  climrec  40359  climsuse  40364  mullimc  40372  mullimcf  40379  constlimc  40380  idlimc  40382  divcnvg  40383  limcperiod  40384  limcrecl  40385  lptioo2  40387  lptioo1  40388  islpcn  40395  lptre2pt  40396  limcleqr  40400  neglimc  40403  addlimc  40404  0ellimcdiv  40405  limclner  40407  climleltrp  40432  limsuplesup  40455  limsupmnflem  40476  supcnvlimsupmpt  40497  0cnv  40498  xlimconst  40575  sinaover2ne0  40603  cncfshift  40611  cncfperiod  40616  cncfioobdlem  40633  cncfioobd  40634  fperdvper  40657  dvdivbd  40662  dvbdfbdioolem1  40667  dvbdfbdioolem2  40668  ioodvbdlimc1lem1  40670  ioodvbdlimc1lem2  40671  ioodvbdlimc2lem  40673  dvnmul  40682  dvnprodlem1  40685  itgiccshift  40719  itgperiod  40720  ismbl3  40726  ovolsplit  40728  stoweidlem1  40741  stoweidlem11  40751  stoweidlem13  40753  stoweidlem14  40754  stoweidlem16  40756  stoweidlem21  40761  stoweidlem25  40765  stoweidlem26  40766  stoweidlem36  40776  stoweidlem38  40778  stoweidlem41  40781  stoweidlem42  40782  stoweidlem45  40785  stoweidlem48  40788  stoweidlem52  40792  stoweidlem62  40802  wallispilem3  40807  stirlinglem5  40818  stirlinglem6  40819  stirlinglem7  40820  stirlinglem10  40823  stirlinglem12  40825  stirlinglem15  40828  dirkercncflem1  40843  fourierdlem10  40857  fourierdlem12  40859  fourierdlem15  40862  fourierdlem16  40863  fourierdlem19  40866  fourierdlem20  40867  fourierdlem21  40868  fourierdlem22  40869  fourierdlem24  40871  fourierdlem30  40877  fourierdlem37  40884  fourierdlem39  40886  fourierdlem40  40887  fourierdlem41  40888  fourierdlem42  40889  fourierdlem47  40893  fourierdlem48  40894  fourierdlem49  40895  fourierdlem50  40896  fourierdlem52  40898  fourierdlem54  40900  fourierdlem60  40906  fourierdlem61  40907  fourierdlem63  40909  fourierdlem64  40910  fourierdlem68  40914  fourierdlem71  40917  fourierdlem72  40918  fourierdlem73  40919  fourierdlem74  40920  fourierdlem75  40921  fourierdlem76  40922  fourierdlem77  40923  fourierdlem78  40924  fourierdlem79  40925  fourierdlem81  40927  fourierdlem82  40928  fourierdlem83  40929  fourierdlem84  40930  fourierdlem87  40933  fourierdlem92  40938  fourierdlem93  40939  fourierdlem94  40940  fourierdlem101  40947  fourierdlem102  40948  fourierdlem103  40949  fourierdlem104  40950  fourierdlem111  40957  fourierdlem112  40958  fourierdlem113  40959  fourierdlem114  40960  sqwvfoura  40968  sqwvfourb  40969  fouriersw  40971  elaa2lem  40973  etransclem23  40997  etransclem28  41002  etransclem32  41006  etransclem35  41009  etransclem48  41022  qndenserrnbllem  41037  rrnprjdstle  41044  ioorrnopnlem  41047  ioorrnopnxrlem  41049  salexct  41075  sge0fsum  41127  sge0supre  41129  sge0rnbnd  41133  sge0lefi  41138  sge0lessmpt  41139  sge0ltfirp  41140  sge0prle  41141  sge0resrnlem  41143  sge0le  41147  sge0split  41149  sge0iunmptlemre  41155  sge0iunmpt  41158  sge0isum  41167  sge0xaddlem1  41173  sge0xaddlem2  41174  sge0xadd  41175  sge0reuz  41187  sge0reuzb  41188  meaunle  41204  meaiunlelem  41208  voliunsge0lem  41212  meaiuninc  41221  meaiininclem  41226  omeunle  41256  omeiunle  41257  omelesplit  41258  omeiunltfirp  41259  carageniuncllem2  41262  caratheodorylem2  41267  caragencmpl  41275  ovnlecvr  41298  ovncvrrp  41304  ovnsubaddlem1  41310  ovnsubadd  41312  hoidmv1lelem1  41331  hoidmv1lelem2  41332  hoidmv1le  41334  hoidmvlelem1  41335  hoidmvlelem2  41336  hoidmvlelem5  41339  hoidmvle  41340  ovnhoilem1  41341  ovnlecvr2  41350  ovncvr2  41351  hoiqssbllem2  41363  hspmbllem2  41367  hspmbllem3  41368  ovnsplit  41388  ovolval5lem1  41392  vonioolem1  41420  vonioolem2  41421  vonicclem1  41423  vonicclem2  41424  pimconstlt1  41441  smflimlem2  41506  smflimlem4  41508  smfmullem1  41524  smfsuplem1  41543  smflimsuplem4  41555  smflimsuplem5  41556  iccpartltu  41913  iccpartleu  41916  pgrple2abl  42698  difmodm1lt  42869  nnpw2blen  42926  dignn0flhalflem1  42961
  Copyright terms: Public domain W3C validator