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

Theorem eqbrtrd 4599
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 4587 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 245 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  eqbrtrrd  4601  somin2  5437  en1b  7887  domunsncan  7922  fodomfi  8101  hartogslem1  8307  wemaplem2  8312  infdifsn  8414  carddomi2  8656  cdaun  8854  cda1dif  8858  mapcdaen  8866  cdaxpdom  8871  cdafi  8872  cdainf  8874  carden  9229  alephsuc3  9258  fpwwe2lem6  9313  fpwwe2lem7  9314  inar1  9453  rankcf  9455  lesub3d  10494  lbinfle  10827  supadd  10838  supmul  10842  rpnnen1lem3  11648  rpnnen1lem3OLD  11654  divge1  11730  xrmin1  11841  xrmin2  11842  ifle  11861  qbtwnxr  11864  xltnegi  11880  xleadd1a  11912  xlt2add  11919  xlemul1a  11947  xov1plusxeqvd  12145  ubmelm1fzo  12385  flflp1  12425  ceim1l  12463  ceilm1lt  12464  ceille  12466  quoremz  12471  quoremnn0ALT  12473  modlt  12496  modeqmodmin  12557  addmodlteq  12562  seqf1olem1  12657  bernneq  12807  discr  12818  faclbnd2  12895  faclbnd4lem3  12899  hashun2  12985  hashfun  13036  ccatsymb  13165  ccatrn  13171  sqrlem6  13782  sqrlem7  13783  rddif  13874  amgm2  13903  icodiamlt  13968  climconst  14068  rlimconst  14069  serclim0  14102  rlimcn1  14113  mulcn2  14120  reccn2  14121  o1mul  14139  o1rlimmul  14143  iserex  14181  climlec2  14183  iserge0  14185  climcau  14195  caucvgrlem  14197  caucvgr  14200  iseraltlem2  14207  iseraltlem3  14208  iseralt  14209  fsumabs  14320  o1fsum  14332  iserabs  14334  climfsum  14339  isumless  14362  climcndslem2  14367  divrcnv  14369  flo1  14371  supcvg  14373  georeclim  14388  geomulcvg  14392  cvgrat  14400  mertenslem1  14401  prodfclim1  14410  fprodge1  14511  fprodle  14512  efcvgfsum  14601  eftlub  14624  eflegeo  14636  tanhlt1  14675  tanhbnd  14676  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos01gt0  14706  ruclem2  14746  ruclem3  14747  ruclem9  14752  ruclem11  14754  ruclem12  14755  bitsfzolem  14940  bitsfzo  14941  bitsinv1lem  14947  sadcaddlem  14963  mulgcd  15049  eucalglt  15082  lcmledvds  15096  lcmfledvds  15129  mulgcddvds  15153  coprmproddvdslem  15160  prmind2  15182  isprm5  15203  divdenle  15241  nonsq  15251  pythagtriplem4  15308  pclem  15327  pcpremul  15332  pczdvds  15351  pcprmpw2  15370  qexpz  15389  prmreclem4  15407  prmreclem5  15408  4sqlem10  15435  ramtub  15500  ramub2  15502  prmodvdslcmf  15535  prmgaplem8  15546  natpropd  16405  catciso  16526  p0le  16812  acsdomd  16950  qusgrp  17418  f1otrspeq  17636  pmtrfrn  17647  pmtrfconj  17655  symggen  17659  psgnunilem4  17686  oddvds2  17752  odcau  17788  pgpfi  17789  pgpssslw  17798  sylow3lem4  17814  efgred2  17935  frgp0  17942  odadd2  18021  oddvdssubg  18027  ablfac1c  18239  ablfac1eu  18241  pgpfaclem3  18251  isabvd  18589  abvsubtri  18604  mplsubrg  19207  coe1sfi  19350  cyggic  19685  mp2pm2mplem5  20376  en2top  20542  1stcrest  21008  2ndcrest  21009  hausmapdom  21055  ufilen  21486  xmetrtri2  21912  prdsxmetlem  21924  bl2in  21956  xblcntrps  21966  xblcntr  21967  ssblps  21978  ssbl  21979  blssps  21980  blss  21981  blcld  22061  methaus  22076  metustexhalf  22112  nmtri2  22181  nrginvrcnlem  22238  nrginvrcn  22239  nmoi  22274  nmo0  22281  nmoid  22288  blcvx  22341  reperflem  22361  reconnlem2  22370  metdcnlem  22379  metdscn  22398  metnrmlem3  22403  mulc1cncf  22447  iccpnfhmeo  22483  cnheiborlem  22492  cnheibor  22493  lebnumii  22504  pcopt  22561  pcopt2  22562  pcoass  22563  nmoleub2lem  22653  nmoleub2lem3  22654  nmoleub2lem2  22655  ipcau2  22762  tchcphlem1  22763  trirn  22908  rrxdstprj1  22917  minveclem3  22925  ivthlem2  22945  ivthlem3  22946  ivth2  22948  ovollb  22971  ovolsslem  22976  ovollb2lem  22980  ovolctb  22982  ovoliunlem1  22994  ovolsca  23007  ovolicc1  23008  ovolicc2lem4  23012  nulmbl  23027  ioombl1lem4  23053  uniioovol  23070  uniioombllem3a  23075  uniioombllem4  23077  opnmbllem  23092  volcn  23097  volivth  23098  i1fadd  23185  i1fmul  23186  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  itg2const2  23231  itg2seq  23232  itg2uba  23233  itg2split  23239  itg2monolem1  23240  itg2monolem3  23242  itg2i1fseq2  23246  itg2addlem  23248  itg2gt0  23250  itg2cnlem1  23251  itg2cnlem2  23252  itgless  23306  ibladdlem  23309  bddmulibl  23328  dveflem  23463  dvferm1lem  23468  dvferm2lem  23470  dvlip  23477  dvlipcn  23478  dvlip2  23479  dvle  23491  dvivthlem1  23492  lhop1lem  23497  dvcvx  23504  dvfsumabs  23507  dvfsumlem2  23511  dvfsumlem4  23513  dvfsumrlim2  23516  dvfsum2  23518  ftc1a  23521  ftc1lem4  23523  ftc1lem5  23524  deg1sub  23589  ply1divex  23617  deg1submon1p  23633  r1pdeglt  23639  dvdsq1p  23641  fta1glem2  23647  fta1g  23648  plyeq0lem  23687  dgrlt  23743  fta1lem  23783  aalioulem2  23809  aalioulem3  23810  aalioulem4  23811  aaliou3lem2  23819  aaliou3lem9  23826  taylply2  23843  ulmbdd  23873  ulmdvlem1  23875  mtest  23879  mtestbdd  23880  radcnvlem1  23888  radcnvle  23895  pserulm  23897  psercn  23901  pserdvlem2  23903  abelthlem2  23907  abelthlem5  23910  abelthlem7  23913  abelthlem8  23914  abelthlem9  23915  reeff1olem  23921  tangtx  23978  tanord  24005  efif1olem4  24012  logrnaddcl  24042  logcj  24073  logimul  24081  logneg2  24082  logdivlti  24087  divlogrlim  24098  logcnlem3  24107  logcnlem4  24108  efopn  24121  logtayllem  24122  logtayl  24123  cxpcn3lem  24205  cxpaddle  24210  abscxpbnd  24211  asinlem3  24315  asinneg  24330  asinsin  24336  atanlogaddlem  24357  atantan  24367  bndatandm  24373  atans2  24375  atantayl  24381  atantayl2  24382  atantayl3  24383  leibpi  24386  birthdaylem3  24397  rlimcnp  24409  efrlim  24413  cxplim  24415  cxp2lim  24420  cxploglim2  24422  divsqrtsumo1  24427  jensenlem2  24431  amgm  24434  logdifbnd  24437  harmonicbnd4  24454  fsumharmonic  24455  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamgulmlem5  24476  lgambdd  24480  lgamcvg2  24498  ftalem1  24516  ftalem5  24520  basellem1  24524  basellem8  24531  ppip1le  24604  ppiltx  24620  sqff1o  24625  chtublem  24653  chpub  24662  logfaclbnd  24664  logfacrlim  24666  logexprlim  24667  mersenne  24669  bcmono  24719  bcmax  24720  bposlem2  24727  bposlem5  24730  lgslem3  24741  gausslemma2dlem1a  24807  lgsquadlem1  24822  lgsquadlem2  24823  2lgslem1c  24835  2sqblem  24873  chebbnd1  24878  chtppilimlem1  24879  chto1ub  24882  chpchtlim  24885  chpo1ubb  24887  rplogsumlem1  24890  rplogsumlem2  24891  rpvmasumlem  24893  dchrisumlem1  24895  dchrisumlem2  24896  dchrmusum2  24900  dchrvmasumlem2  24904  dchrvmasumlem3  24905  dchrvmasumiflem1  24907  dchrisum0flblem1  24914  dchrisum0fno1  24917  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2a  24923  dchrisum0lem2  24924  rplogsum  24933  mudivsum  24936  mulogsumlem  24937  mulog2sumlem1  24940  mulog2sumlem2  24941  vmalogdivsum2  24944  2vmadivsumlem  24946  selberglem2  24952  selberg2b  24958  logdivbnd  24962  selberg3lem1  24963  selberg3lem2  24964  selberg4lem1  24966  pntrmax  24970  pntrsumo1  24971  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bnd  24990  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem2  24997  pntlemb  25003  pntlemg  25004  pntlemh  25005  pntlemr  25008  pntlemj  25009  pntlemf  25011  pntlemo  25013  pnt  25020  padicabv  25036  ostth2lem2  25040  ostth2lem3  25041  ostth3  25044  colperpexlem3  25342  mideulem2  25344  lnperpex  25413  trgcopy  25414  iscgra1  25420  brbtwn2  25503  colinearalglem4  25507  nvmtri2  26705  nvabs  26706  nvge0  26707  nvlmle  26732  smcnlem  26737  nmblolbii  26844  blocnilem  26849  siii  26898  ubthlem2  26917  minvecolem3  26922  htthlem  26964  bcsiALT  27226  bcs3  27230  chscllem4  27689  0cnop  28028  0cnfn  28029  nmbdoplbi  28073  nmcoplbi  28077  nmophmi  28080  nmbdfnlbi  28098  nmcfnlbi  28101  nlelchi  28110  riesz1  28114  cnlnadjlem2  28117  nmopadjlei  28137  nmoptrii  28143  nmopcoi  28144  nmopcoadji  28150  unierri  28153  branmfn  28154  pjs14i  28259  hstle  28279  cdj3lem2b  28486  xlt2addrd  28719  eliccelico  28735  elicoelioo  28736  ltesubnnd  28761  archirngz  28880  archiabllem2c  28886  madjusmdetlem2  29028  locfinref  29042  sqsscirc1  29088  tpr2rico  29092  esumcst  29258  esumgect  29285  esum2d  29288  measunl  29412  measiun  29414  omssubaddlem  29494  omssubadd  29495  carsgsigalem  29510  carsgclctunlem2  29514  pmeasmono  29519  eulerpartlemgc  29557  eulerpartlemb  29563  ballotlemsel1i  29707  ballotlemro  29717  sgnsub  29739  signsplypnf  29759  signsply0  29760  signsvtn  29793  signsvfnn  29795  erdsze2lem1  30245  sinccvglem  30626  divcnvlin  30677  iprodefisum  30686  faclimlem2  30689  nodense  30894  nobnddown  30906  fnemeet1  31337  dnibndlem10  31453  dnibndlem11  31454  dnibnd  31457  knoppcnlem4  31462  knoppcnlem6  31464  unblimceq0lem  31473  unblimceq0  31474  unbdqndv2lem1  31476  unbdqndv2lem2  31477  knoppndvlem11  31489  knoppndvlem12  31490  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem18  31496  knoppndvlem19  31497  knoppndvlem21  31499  ltflcei  32363  ptrecube  32375  poimirlem16  32391  poimirlem17  32392  poimirlem29  32404  broucube  32409  opnmbllem0  32411  mblfinlem2  32413  mblfinlem3  32414  ismblfin  32416  itg2addnclem  32427  itg2addnclem2  32428  itg2addnclem3  32429  itg2addnc  32430  ibladdnclem  32432  ftc1cnnclem  32449  ftc1cnnc  32450  ftc1anc  32459  geomcau  32521  prdsbnd  32558  cntotbnd  32561  heiborlem4  32579  rrndstprj2  32596  rrncmslem  32597  rrnequiv  32600  iccbnd  32605  cvlcvr1  33440  cvrat3  33542  dalem25  33798  cdlema1N  33891  dalawlem3  33973  dalawlem4  33974  dalawlem5  33975  dalawlem6  33976  dalawlem7  33977  dalawlem9  33979  dalawlem11  33981  dalawlem12  33982  lhp2lt  34101  lhpmcvr  34123  4atexlemcnd  34172  lautj  34193  trlle  34285  trlval3  34288  trlval4  34289  cdleme0moN  34326  cdleme13  34373  cdleme15  34379  cdleme19b  34406  cdleme20e  34415  cdleme20j  34420  cdleme22e  34446  cdleme22eALTN  34447  cdleme26fALTN  34464  cdleme26f  34465  cdleme27N  34471  cdleme41sn3a  34535  cdleme46fsvlpq  34607  cdlemeg46vrg  34629  cdlemg4  34719  cdlemg7N  34728  cdlemg9a  34734  cdlemg11b  34744  cdlemg12a  34745  trljco  34842  tendoidcl  34871  tendococl  34874  tendopltp  34882  tendo0tp  34891  tendoicl  34898  cdlemi2  34921  cdlemk5a  34937  cdlemk5  34938  cdlemk12  34952  cdlemkole  34955  cdlemk14  34956  cdlemk12u  34974  cdlemk37  35016  cdlemk39s-id  35042  cdlemk49  35053  cdlemk39u1  35069  cdlemk39u  35070  dian0  35142  cdlemm10N  35221  cdlemn2  35298  cdlemn10  35309  dihord1  35321  dihord10  35326  dihmeetlem4preN  35409  dihmeetlem18N  35427  dihmeetlem20N  35429  dihjatc  35520  mapdcnvatN  35769  lzenom  36147  irrapxlem2  36201  irrapxlem3  36202  irrapxlem5  36204  pellexlem2  36208  pell14qrgt0  36237  pellfundlb  36262  pellfundex  36264  pellfund14  36276  rmspecsqrtnq  36284  rmspecsqrtnqOLD  36285  jm2.24nn  36340  jm2.17a  36341  jm2.17b  36342  congabseq  36355  acongrep  36361  acongeq  36364  jm2.26lem3  36382  jm2.27a  36386  jm2.27c  36388  hbtlem2  36509  dgraaub  36533  idomodle  36589  relexpxpmin  36824  frege102d  36861  hashnzfzclim  37339  binomcxplemfrat  37368  binomcxplemnotnn0  37373  suprnmpt  38146  mpct  38184  dstregt0  38230  lefldiveq  38242  fzisoeu  38251  upbdrech  38256  ssfiunibd  38260  fzdifsuc2  38263  xadd0ge  38274  supxrgere  38287  supxrge  38292  suplesup  38293  xrlexaddrp  38306  infxrunb2  38322  infleinflem2  38325  reclt0d  38345  ioondisj2  38358  iccshift  38388  iooshift  38392  fmul01  38444  fmul01lt1lem1  38448  fmul01lt1lem2  38449  climrec  38467  climsuse  38472  mullimc  38480  mullimcf  38487  constlimc  38488  idlimc  38490  divcnvg  38491  limcperiod  38492  limcrecl  38493  lptioo2  38495  lptioo1  38496  islpcn  38503  lptre2pt  38504  limcleqr  38508  neglimc  38511  addlimc  38512  0ellimcdiv  38513  limclner  38515  climleltrp  38540  sinaover2ne0  38548  cncfshift  38556  cncfperiod  38561  cncfioobdlem  38579  cncfioobd  38580  fperdvper  38605  dvdivbd  38610  dvbdfbdioolem1  38615  dvbdfbdioolem2  38616  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnmul  38630  dvnprodlem1  38633  itgiccshift  38669  itgperiod  38670  ismbl3  38676  ovolsplit  38678  stoweidlem1  38691  stoweidlem11  38701  stoweidlem13  38703  stoweidlem14  38704  stoweidlem16  38706  stoweidlem21  38711  stoweidlem25  38715  stoweidlem26  38716  stoweidlem36  38726  stoweidlem38  38728  stoweidlem41  38731  stoweidlem42  38732  stoweidlem45  38735  stoweidlem48  38738  stoweidlem52  38742  stoweidlem62  38752  wallispilem3  38757  stirlinglem5  38768  stirlinglem6  38769  stirlinglem7  38770  stirlinglem10  38773  stirlinglem12  38775  stirlinglem15  38778  dirkercncflem1  38793  fourierdlem10  38807  fourierdlem12  38809  fourierdlem15  38812  fourierdlem16  38813  fourierdlem19  38816  fourierdlem20  38817  fourierdlem21  38818  fourierdlem22  38819  fourierdlem24  38821  fourierdlem30  38827  fourierdlem37  38834  fourierdlem39  38836  fourierdlem40  38837  fourierdlem41  38838  fourierdlem42  38839  fourierdlem47  38843  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem52  38848  fourierdlem54  38850  fourierdlem60  38856  fourierdlem61  38857  fourierdlem63  38859  fourierdlem64  38860  fourierdlem68  38864  fourierdlem71  38867  fourierdlem72  38868  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem77  38873  fourierdlem78  38874  fourierdlem79  38875  fourierdlem81  38877  fourierdlem82  38878  fourierdlem83  38879  fourierdlem84  38880  fourierdlem87  38883  fourierdlem92  38888  fourierdlem93  38889  fourierdlem94  38890  fourierdlem101  38897  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem112  38908  fourierdlem113  38909  fourierdlem114  38910  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  elaa2lem  38923  etransclem23  38947  etransclem28  38952  etransclem32  38956  etransclem35  38959  etransclem48  38972  qndenserrnbllem  38987  rrnprjdstle  38994  ioorrnopnlem  38997  ioorrnopnxrlem  38999  salexct  39025  sge0fsum  39077  sge0supre  39079  sge0rnbnd  39083  sge0lefi  39088  sge0lessmpt  39089  sge0ltfirp  39090  sge0prle  39091  sge0resrnlem  39093  sge0le  39097  sge0split  39099  sge0iunmptlemre  39105  sge0iunmpt  39108  sge0isum  39117  sge0xaddlem1  39123  sge0xaddlem2  39124  sge0xadd  39125  sge0reuz  39137  sge0reuzb  39138  meaunle  39154  meaiunlelem  39158  voliunsge0lem  39162  meaiuninc  39171  meaiininclem  39173  omeunle  39203  omeiunle  39204  omelesplit  39205  omeiunltfirp  39206  carageniuncllem2  39209  caratheodorylem2  39214  caragencmpl  39222  ovnlecvr  39245  ovncvrrp  39251  ovnsubaddlem1  39257  ovnsubadd  39259  hoidmv1lelem1  39278  hoidmv1lelem2  39279  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem5  39286  hoidmvle  39287  ovnhoilem1  39288  ovnlecvr2  39297  ovncvr2  39298  hoiqssbllem2  39310  hspmbllem2  39314  hspmbllem3  39315  ovnsplit  39335  ovolval5lem1  39339  vonioolem1  39368  vonioolem2  39369  vonicclem1  39371  vonicclem2  39372  pimconstlt1  39389  smflimlem2  39455  smflimlem4  39457  smfmullem1  39473  iccpartltu  39761  iccpartleu  39764  subupgr  40506  crctcsh1wlkn0lem1  41008  pgrple2abl  41935  difmodm1lt  42106  nnpw2blen  42167  dignn0flhalflem1  42202
  Copyright terms: Public domain W3C validator