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

Theorem eqbrtrd 5055
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 5043 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 260 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538   class class class wbr 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034
This theorem is referenced by:  eqbrtrrd  5057  somin2  5966  en1b  8564  domunsncan  8604  fodomfi  8785  infsupprpr  8956  hartogslem1  8994  wemaplem2  8999  infdifsn  9108  carddomi2  9387  djuinf  9603  carden  9966  alephsuc3  9995  fpwwe2lem6  10050  fpwwe2lem7  10051  inar1  10190  rankcf  10192  lesub3d  11251  lbinfle  11587  supadd  11600  supmul  11604  rpnnen1lem3  12370  divge1  12449  xrmin1  12562  xrmin2  12563  ifle  12582  qbtwnxr  12585  xltnegi  12601  xleadd1a  12638  xlt2add  12645  xlemul1a  12673  xov1plusxeqvd  12880  ubmelm1fzo  13132  flflp1  13176  ceim1l  13214  ceilm1lt  13215  ceille  13217  quoremz  13222  quoremnn0ALT  13224  modlt  13247  modeqmodmin  13308  addmodlteq  13313  seqf1olem1  13409  bernneq  13590  discr  13601  faclbnd2  13651  faclbnd4lem3  13655  hashun2  13744  hashfun  13798  ccatsymb  13931  ccatrn  13938  sqrlem6  14603  sqrlem7  14604  rddif  14696  amgm2  14725  icodiamlt  14791  climconst  14896  rlimconst  14897  serclim0  14930  rlimcn1  14941  mulcn2  14948  reccn2  14949  o1mul  14967  o1rlimmul  14971  iserex  15009  climlec2  15011  iserge0  15013  climcau  15023  caucvgrlem  15025  caucvgr  15028  iseraltlem2  15035  iseraltlem3  15036  iseralt  15037  fsumabs  15152  o1fsum  15164  iserabs  15166  climfsum  15171  isumless  15196  climcndslem2  15201  divrcnv  15203  flo1  15205  supcvg  15207  georeclim  15224  geomulcvg  15228  cvgrat  15235  mertenslem1  15236  prodfclim1  15245  fprodle  15346  efcvgfsum  15435  eftlub  15458  eflegeo  15470  tanhlt1  15509  tanhbnd  15510  ef01bndlem  15533  sin01bnd  15534  cos01bnd  15535  cos01gt0  15540  ruclem2  15581  ruclem3  15582  ruclem9  15587  ruclem11  15589  ruclem12  15590  bitsfzolem  15777  bitsfzo  15778  bitsinv1lem  15784  sadcaddlem  15800  mulgcd  15890  eucalglt  15923  lcmledvds  15937  lcmfledvds  15970  mulgcddvds  15993  coprmproddvdslem  16000  prmind2  16023  isprm5  16045  divdenle  16083  nonsq  16093  pythagtriplem4  16150  pclem  16169  pcpremul  16174  pczdvds  16193  pcprmpw2  16212  qexpz  16231  prmreclem4  16249  prmreclem5  16250  4sqlem10  16277  ramtub  16342  ramub2  16344  prmodvdslcmf  16377  prmgaplem8  16388  natpropd  17242  catciso  17363  p0le  17649  acsdomd  17787  triv1nsgd  18321  qusgrp  18331  f1otrspeq  18571  pmtrfrn  18582  pmtrfconj  18590  symggen  18594  psgnunilem4  18621  oddvds2  18689  odcau  18725  pgpfi  18726  pgpssslw  18735  sylow3lem4  18751  efgred2  18875  frgp0  18882  odadd2  18966  oddvdssubg  18972  ablfac1c  19190  ablfac1eu  19192  pgpfaclem3  19202  2nsgsimpgd  19221  isabvd  19588  abvsubtri  19603  cyggic  20268  mplsubrg  20682  coe1sfi  20846  mp2pm2mplem5  21419  en2top  21594  1stcrest  22062  2ndcrest  22063  hausmapdom  22109  ufilen  22539  xmetrtri2  22967  prdsxmetlem  22979  bl2in  23011  xblcntrps  23021  xblcntr  23022  ssblps  23033  ssbl  23034  blssps  23035  blss  23036  blcld  23116  methaus  23131  metustexhalf  23167  nmtri2  23237  tngngp3  23266  nrginvrcnlem  23301  nrginvrcn  23302  nmoi  23338  nmo0  23345  nmoid  23352  blcvx  23407  reperflem  23427  reconnlem2  23436  metdcnlem  23445  metdscn  23465  metnrmlem3  23470  mulc1cncf  23514  iccpnfhmeo  23554  cnheiborlem  23563  cnheibor  23564  lebnumii  23575  pcopt  23631  pcopt2  23632  pcoass  23633  nmoleub2lem  23723  nmoleub2lem3  23724  nmoleub2lem2  23725  ipcau2  23842  tcphcphlem1  23843  nglmle  23910  trirn  24008  rrxdstprj1  24017  minveclem3  24037  ivthlem2  24060  ivthlem3  24061  ivth2  24063  ovollb  24087  ovolsslem  24092  ovollb2lem  24096  ovolctb  24098  ovoliunlem1  24110  ovolsca  24123  ovolicc1  24124  ovolicc2lem4  24128  nulmbl  24143  ioombl1lem4  24169  uniioovol  24187  uniioombllem3a  24192  uniioombllem4  24194  opnmbllem  24209  volcn  24214  volivth  24215  i1fadd  24303  i1fmul  24304  mbfi1fseqlem4  24326  mbfi1fseqlem5  24327  mbfi1fseqlem6  24328  itg2const2  24349  itg2seq  24350  itg2uba  24351  itg2split  24357  itg2monolem1  24358  itg2monolem3  24360  itg2i1fseq2  24364  itg2addlem  24366  itg2gt0  24368  itg2cnlem1  24369  itg2cnlem2  24370  itgless  24424  ibladdlem  24427  bddmulibl  24446  dveflem  24586  dvferm1lem  24591  dvferm2lem  24593  dvlip  24600  dvlipcn  24601  dvlip2  24602  dvle  24614  dvivthlem1  24615  lhop1lem  24620  dvcvx  24627  dvfsumabs  24630  dvfsumlem2  24634  dvfsumlem4  24636  dvfsumrlim2  24639  dvfsum2  24641  ftc1a  24644  ftc1lem4  24646  ftc1lem5  24647  deg1sub  24713  ply1divex  24741  deg1submon1p  24757  r1pdeglt  24763  dvdsq1p  24765  fta1glem2  24771  fta1g  24772  plyeq0lem  24811  dgrlt  24867  fta1lem  24907  aalioulem2  24933  aalioulem3  24934  aalioulem4  24935  aaliou3lem2  24943  aaliou3lem9  24950  taylply2  24967  ulmbdd  24997  ulmdvlem1  24999  mtest  25003  mtestbdd  25004  radcnvlem1  25012  radcnvle  25019  pserulm  25021  psercn  25025  pserdvlem2  25027  abelthlem2  25031  abelthlem5  25034  abelthlem7  25037  abelthlem8  25038  abelthlem9  25039  reeff1olem  25045  tangtx  25102  tanord  25134  efif1olem4  25141  logrnaddcl  25170  logcj  25201  logimul  25209  logneg2  25210  logdivlti  25215  divlogrlim  25230  logcnlem3  25239  logcnlem4  25240  efopn  25253  logtayllem  25254  logtayl  25255  cxpcn3lem  25340  cxpaddle  25345  abscxpbnd  25346  asinlem3  25461  asinneg  25476  asinsin  25482  atanlogaddlem  25503  atantan  25513  bndatandm  25519  atans2  25521  atantayl  25527  atantayl2  25528  atantayl3  25529  leibpi  25532  birthdaylem3  25543  rlimcnp  25555  efrlim  25559  cxplim  25561  cxp2lim  25566  cxploglim2  25568  divsqrtsumo1  25573  jensenlem2  25577  amgm  25580  logdifbnd  25583  harmonicbnd4  25600  fsumharmonic  25601  lgamgulmlem2  25619  lgamgulmlem3  25620  lgamgulmlem5  25622  lgambdd  25626  lgamcvg2  25644  ftalem1  25662  ftalem5  25666  basellem1  25670  basellem8  25677  ppip1le  25750  ppiltx  25766  sqff1o  25771  chtublem  25799  chpub  25808  logfaclbnd  25810  logfacrlim  25812  logexprlim  25813  mersenne  25815  bcmono  25865  bcmax  25866  bposlem2  25873  bposlem5  25876  lgslem3  25887  gausslemma2dlem1a  25953  lgsquadlem1  25968  lgsquadlem2  25969  2lgslem1c  25981  2sqblem  26019  chebbnd1  26060  chtppilimlem1  26061  chto1ub  26064  chpchtlim  26067  chpo1ubb  26069  rplogsumlem1  26072  rplogsumlem2  26073  rpvmasumlem  26075  dchrisumlem1  26077  dchrisumlem2  26078  dchrmusum2  26082  dchrvmasumlem2  26086  dchrvmasumlem3  26087  dchrvmasumiflem1  26089  dchrisum0flblem1  26096  dchrisum0fno1  26099  dchrisum0lem1b  26103  dchrisum0lem1  26104  dchrisum0lem2a  26105  dchrisum0lem2  26106  rplogsum  26115  mudivsum  26118  mulogsumlem  26119  mulog2sumlem1  26122  mulog2sumlem2  26123  vmalogdivsum2  26126  2vmadivsumlem  26128  selberglem2  26134  selberg2b  26140  logdivbnd  26144  selberg3lem1  26145  selberg3lem2  26146  selberg4lem1  26148  pntrmax  26152  pntrsumo1  26153  pntrlog2bndlem1  26165  pntrlog2bndlem2  26166  pntrlog2bndlem3  26167  pntrlog2bndlem4  26168  pntrlog2bndlem5  26169  pntrlog2bnd  26172  pntpbnd1a  26173  pntpbnd2  26175  pntibndlem2  26179  pntlemb  26185  pntlemg  26186  pntlemh  26187  pntlemr  26190  pntlemj  26191  pntlemf  26193  pntlemo  26195  pnt  26202  padicabv  26218  ostth2lem2  26222  ostth2lem3  26223  ostth3  26226  colperpexlem3  26530  mideulem2  26532  lnperpex  26601  trgcopy  26602  iscgra1  26608  brbtwn2  26703  colinearalglem4  26707  subupgr  27081  crctcshwlkn0lem1  27600  nvabs  28459  nvge0  28460  smcnlem  28484  nmblolbii  28586  blocnilem  28591  siii  28640  ubthlem2  28658  minvecolem3  28663  htthlem  28704  bcsiALT  28966  bcs3  28970  chscllem4  29427  0cnop  29766  0cnfn  29767  nmbdoplbi  29811  nmcoplbi  29815  nmophmi  29818  nmbdfnlbi  29836  nmcfnlbi  29839  nlelchi  29848  riesz1  29852  cnlnadjlem2  29855  nmopadjlei  29875  nmoptrii  29881  nmopcoi  29882  nmopcoadji  29888  unierri  29891  branmfn  29892  pjs14i  29997  hstle  30017  cdj3lem2b  30224  xlt2addrd  30512  eliccelico  30530  elicoelioo  30531  ltesubnnd  30568  wrdt2ind  30657  archirngz  30872  archiabllem2c  30878  madjusmdetlem2  31185  locfinref  31198  sqsscirc1  31265  tpr2rico  31269  esumcst  31436  esumgect  31463  esum2d  31466  measunl  31589  measiun  31591  omssubaddlem  31671  omssubadd  31672  carsgsigalem  31687  carsgclctunlem2  31691  pmeasmono  31696  eulerpartlemgc  31734  eulerpartlemb  31740  ballotlemsel1i  31884  ballotlemro  31894  sgnsub  31916  signsplypnf  31934  signsply0  31935  signsvtn  31968  signsvfnn  31970  hgt750lemd  32033  logdivsqrle  32035  hashf1dmcdm  32470  erdsze2lem1  32564  sinccvglem  33029  divcnvlin  33078  iprodefisum  33087  faclimlem2  33090  nosep1o  33300  nodense  33310  fnemeet1  33828  dnibndlem10  33940  dnibndlem11  33941  dnibnd  33944  knoppcnlem4  33949  knoppcnlem6  33951  unblimceq0lem  33959  unbdqndv2lem1  33962  unbdqndv2lem2  33963  knoppndvlem11  33975  knoppndvlem12  33976  knoppndvlem14  33978  knoppndvlem15  33979  knoppndvlem17  33981  knoppndvlem18  33982  knoppndvlem19  33983  knoppndvlem21  33985  ctbssinf  34824  ltflcei  35044  ptrecube  35056  poimirlem16  35072  poimirlem17  35073  poimirlem29  35085  broucube  35090  opnmbllem0  35092  mblfinlem2  35094  mblfinlem3  35095  ismblfin  35097  itg2addnclem  35107  itg2addnclem2  35108  itg2addnclem3  35109  itg2addnc  35110  ibladdnclem  35112  ftc1cnnclem  35127  ftc1cnnc  35128  ftc1anc  35137  geomcau  35196  prdsbnd  35230  cntotbnd  35233  heiborlem4  35251  rrndstprj2  35268  rrncmslem  35269  rrnequiv  35272  iccbnd  35277  cvlcvr1  36634  cvrat3  36737  dalem25  36993  cdlema1N  37086  dalawlem3  37168  dalawlem4  37169  dalawlem5  37170  dalawlem6  37171  dalawlem7  37172  dalawlem9  37174  dalawlem11  37176  dalawlem12  37177  lhp2lt  37296  lhpmcvr  37318  4atexlemcnd  37367  lautj  37388  trlle  37479  trlval3  37482  trlval4  37483  cdleme0moN  37520  cdleme13  37567  cdleme15  37573  cdleme19b  37599  cdleme20e  37608  cdleme20j  37613  cdleme22e  37639  cdleme22eALTN  37640  cdleme26fALTN  37657  cdleme26f  37658  cdleme27N  37664  cdleme41sn3a  37728  cdleme46fsvlpq  37800  cdlemeg46vrg  37822  cdlemg4  37912  cdlemg7N  37921  cdlemg9a  37927  cdlemg11b  37937  cdlemg12a  37938  trljco  38035  tendoidcl  38064  tendococl  38067  tendopltp  38075  tendo0tp  38084  tendoicl  38091  cdlemi2  38114  cdlemk5a  38130  cdlemk5  38131  cdlemk12  38145  cdlemkole  38148  cdlemk14  38149  cdlemk12u  38167  cdlemk37  38209  cdlemk39s-id  38235  cdlemk49  38246  cdlemk39u1  38262  cdlemk39u  38263  dian0  38334  cdlemm10N  38413  cdlemn2  38490  cdlemn10  38501  dihord1  38513  dihord10  38518  dihmeetlem4preN  38601  dihmeetlem18N  38619  dihmeetlem20N  38621  dihjatc  38712  mapdcnvatN  38961  lcmineqlem17  39332  3lexlogpow5ineq2  39341  2ap1caineq  39346  metakunt16  39362  metakunt29  39375  fltltc  39614  lzenom  39708  irrapxlem2  39761  irrapxlem3  39762  irrapxlem5  39764  pellexlem2  39768  pell14qrgt0  39797  pellfundlb  39822  pellfundex  39824  pellfund14  39836  rmspecsqrtnq  39844  jm2.24nn  39897  jm2.17a  39898  jm2.17b  39899  congabseq  39912  acongrep  39918  acongeq  39921  jm2.26lem3  39939  jm2.27a  39943  jm2.27c  39945  hbtlem2  40065  dgraaub  40089  idomodle  40137  sqrtcval  40338  relexpxpmin  40415  frege102d  40452  hashnzfzclim  41023  binomcxplemfrat  41052  binomcxplemnotnn0  41057  suprnmpt  41795  mpct  41827  rnmptbddlem  41878  dstregt0  41909  lefldiveq  41921  fzisoeu  41929  upbdrech  41934  ssfiunibd  41938  fzdifsuc2  41939  xadd0ge  41949  supxrgere  41962  supxrge  41967  suplesup  41968  xrlexaddrp  41981  infxrunb2  41997  infleinflem2  42000  reclt0d  42019  infrpgernmpt  42101  ioondisj2  42127  iccshift  42152  iooshift  42156  fmul01  42219  fmul01lt1lem1  42223  fmul01lt1lem2  42224  climrec  42242  climsuse  42247  mullimc  42255  mullimcf  42262  constlimc  42263  idlimc  42265  divcnvg  42266  limcperiod  42267  limcrecl  42268  lptioo2  42270  lptioo1  42271  islpcn  42278  lptre2pt  42279  limcleqr  42283  neglimc  42286  addlimc  42287  0ellimcdiv  42288  limclner  42290  climleltrp  42315  limsuplesup  42338  limsupmnflem  42359  supcnvlimsupmpt  42380  0cnv  42381  xlimconst  42464  xlimliminflimsup  42501  sinaover2ne0  42507  cncfshift  42513  cncfperiod  42518  cncfioobdlem  42535  cncfioobd  42536  fperdvper  42558  dvdivbd  42562  dvbdfbdioolem1  42567  dvbdfbdioolem2  42568  ioodvbdlimc1lem1  42570  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  dvnmul  42582  dvnprodlem1  42585  itgiccshift  42619  itgperiod  42620  ismbl3  42625  ovolsplit  42627  stoweidlem1  42640  stoweidlem11  42650  stoweidlem13  42652  stoweidlem14  42653  stoweidlem16  42655  stoweidlem21  42660  stoweidlem25  42664  stoweidlem26  42665  stoweidlem36  42675  stoweidlem38  42677  stoweidlem41  42680  stoweidlem42  42681  stoweidlem45  42684  stoweidlem48  42687  stoweidlem52  42691  stoweidlem62  42701  wallispilem3  42706  stirlinglem5  42717  stirlinglem6  42718  stirlinglem7  42719  stirlinglem10  42722  stirlinglem12  42724  stirlinglem15  42727  dirkercncflem1  42742  fourierdlem10  42756  fourierdlem12  42758  fourierdlem15  42761  fourierdlem16  42762  fourierdlem19  42765  fourierdlem20  42766  fourierdlem21  42767  fourierdlem22  42768  fourierdlem24  42770  fourierdlem30  42776  fourierdlem37  42783  fourierdlem39  42785  fourierdlem40  42786  fourierdlem41  42787  fourierdlem42  42788  fourierdlem47  42792  fourierdlem48  42793  fourierdlem49  42794  fourierdlem50  42795  fourierdlem52  42797  fourierdlem54  42799  fourierdlem60  42805  fourierdlem61  42806  fourierdlem63  42808  fourierdlem64  42809  fourierdlem68  42813  fourierdlem71  42816  fourierdlem72  42817  fourierdlem73  42818  fourierdlem74  42819  fourierdlem75  42820  fourierdlem76  42821  fourierdlem77  42822  fourierdlem78  42823  fourierdlem79  42824  fourierdlem81  42826  fourierdlem82  42827  fourierdlem83  42828  fourierdlem84  42829  fourierdlem87  42832  fourierdlem92  42837  fourierdlem93  42838  fourierdlem94  42839  fourierdlem101  42846  fourierdlem102  42847  fourierdlem103  42848  fourierdlem104  42849  fourierdlem111  42856  fourierdlem112  42857  fourierdlem113  42858  fourierdlem114  42859  sqwvfoura  42867  sqwvfourb  42868  fouriersw  42870  elaa2lem  42872  etransclem23  42896  etransclem28  42901  etransclem32  42905  etransclem35  42908  etransclem48  42921  qndenserrnbllem  42933  rrnprjdstle  42940  ioorrnopnlem  42943  ioorrnopnxrlem  42945  salexct  42971  sge0fsum  43023  sge0supre  43025  sge0rnbnd  43029  sge0lefi  43034  sge0lessmpt  43035  sge0ltfirp  43036  sge0prle  43037  sge0resrnlem  43039  sge0le  43043  sge0split  43045  sge0iunmptlemre  43051  sge0iunmpt  43054  sge0isum  43063  sge0xaddlem1  43069  sge0xaddlem2  43070  sge0xadd  43071  sge0reuz  43083  sge0reuzb  43084  meaunle  43100  meaiunlelem  43104  voliunsge0lem  43108  meaiuninc  43117  meaiininclem  43122  omeunle  43152  omeiunle  43153  omelesplit  43154  omeiunltfirp  43155  carageniuncllem2  43158  caratheodorylem2  43163  caragencmpl  43171  ovnlecvr  43194  ovncvrrp  43200  ovnsubaddlem1  43206  ovnsubadd  43208  hoidmv1lelem1  43227  hoidmv1lelem2  43228  hoidmv1le  43230  hoidmvlelem1  43231  hoidmvlelem2  43232  hoidmvlelem5  43235  hoidmvle  43236  ovnhoilem1  43237  ovnlecvr2  43246  ovncvr2  43247  hoiqssbllem2  43259  hspmbllem2  43263  hspmbllem3  43264  ovnsplit  43284  ovolval5lem1  43288  vonioolem1  43316  vonioolem2  43317  vonicclem1  43319  vonicclem2  43320  pimconstlt1  43337  smflimlem2  43402  smflimlem4  43404  smfmullem1  43420  smfsuplem1  43439  smflimsuplem4  43451  smflimsuplem5  43452  iccpartltu  43939  iccpartleu  43942  pgrple2abl  44764  difmodm1lt  44933  nnpw2blen  44991  dignn0flhalflem1  45026  2itscp  45192
  Copyright terms: Public domain W3C validator